1 /-
2 Copyright (c) 2017 Mario Carneiro. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Author: Mario Carneiro
5
6 Finite types.
7 -/
8 import data.finset algebra.big_operators data.array.lemmas logic.unique
src └─────────┘ └───────────────────┘ └───────────────┘ └──────────┘
9 import tactic.wlog
src └─────────┘
10 universes u v
11
12 variables {α : Type*} {β : Type*} {γ : Type*}
13
14 /-- `fintype α` means that `α` is finite, i.e. there are only
15 finitely many distinct elements of type `α`. The evidence of this
16 is a finset `elems` (a list up to permutation without duplicates),
17 together with a proof that everything of type `α` is in the list. -/
18 class fintype (α : Type*) :=
id └───┘
typ └───┘
19 (elems : finset α)
id └────┘ ┴
src └────┘
typ └────┘ ┴
doc └────┘
20 (complete : ∀ x : α, x ∈ elems)
id ┴ ┴ ┴ ┴ └───┘
src ┴
typ ┴ ┴ ┴ ┴ └───┘
21
22 namespace finset
23 variable [fintype α]
id └─────┘
src └─────┘
typ └─────┘
doc └─────┘
24
25 /-- `univ` is the universal finite set of type `finset α` implied from
26 the assumption `fintype α`. -/
27 def univ : finset α := fintype.elems α
id └────┘ ┴ └───────────┘ ┴
src └────┘ └───────────┘
typ └────┘ ┴ └───────────┘ ┴
doc └────┘
28
29 @[simp] theorem mem_univ (x : α) : x ∈ (univ : finset α) :=
id ┴ ┴ ┴ └──┘ └────┘ ┴
src ┴ └──┘ └────┘
typ ┴ ┴ ┴ └──┘ └────┘ ┴
doc └──┘ └──┘ └────┘
30 fintype.complete x
id └──────────────┘ ┴
src └──────────────┘
typ └──────────────┘ ┴
31
32 @[simp] theorem mem_univ_val : ∀ x, x ∈ (univ : finset α).1 := mem_univ
id ┴ ┴ ┴ └──┘ └────┘ ┴ ┴ └──────┘
src ┴ └──┘ └────┘ ┴ └──────┘
typ ┴ ┴ ┴ └──┘ └────┘ ┴ ┴ └──────┘
doc └──┘ └──┘ └────┘
33
34 @[simp] lemma coe_univ : ↑(univ : finset α) = (set.univ : set α) :=
id ┴ └──┘ └────┘ ┴ ┴ └──────┘ └─┘ ┴
src ┴ └──┘ └────┘ ┴ └──────┘ └─┘
typ ┴ └──┘ └────┘ ┴ ┴ └──────┘ └─┘ ┴
doc └──┘ └──┘ └────┘
35 by ext; simp
src └─┘ └────
typ └─┘ └────
doc └─┘ └────
txt └─┘ └────
par └─┘ └────
pid └
st └──────────
36
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
37 theorem subset_univ (s : finset α) : s ⊆ univ := λ a _, mem_univ a
id └────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──────┘ ┴
src └────┘ ┴ └──┘ └──────┘
typ └────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └──────┘ ┴
doc └────┘ └──┘
38
39 theorem eq_univ_iff_forall {s : finset α} : s = univ ↔ ∀ x, x ∈ s :=
id └────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ └──┘ ┴ ┴
typ └────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └────┘ └──┘
40 by simp [ext]
id └─┘
src └────┘└─┘└─
typ └────┘└─┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
41
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
42 @[simp] lemma piecewise_univ [∀i : α, decidable (i ∈ (univ : finset α))]
id ┴ └───────┘ ┴ ┴ └──┘ └────┘ ┴
src └───────┘ ┴ └──┘ └────┘
typ ┴ └───────┘ ┴ ┴ └──┘ └────┘ ┴
doc └──┘ └──┘ └────┘
43 {δ : α → Sort*} (f g : Πi, δ i) : univ.piecewise f g = f :=
id ┴ ┴ ┴ ┴ └──┘└────────┘ ┴ ┴ ┴ ┴
src └──┘└────────┘ ┴
typ ┴ ┴ ┴ ┴ └──┘└────────┘ ┴ ┴ ┴ ┴
doc └──┘└────────┘
44 by { ext i, simp [piecewise] }
id └───────┘
src └───┘ └────┘└───────┘└┘
typ └───┘ └────┘└───────┘└┘
doc └───┘ └────┘└───────┘└┘
txt └───┘ └────┘ └┘
par └───┘ └────┘ └┘
pid └┘ ┴┴ ┴┴
st └──────┘└─────────────────┘└┘
45
46 end finset
47
48 open finset function
49
50 namespace fintype
51
52 instance decidable_pi_fintype {α} {β : α → Type*} [fintype α] [∀a, decidable_eq (β a)] :
id ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴
src └─────┘ └──────────┘
typ ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴
doc └─────┘
53 decidable_eq (Πa, β a) :=
id └──────────┘ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴
54 assume f g, decidable_of_iff (∀ a ∈ fintype.elems α, f a = g a)
id ┴ ┴ └──────────────┘ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────┘ ┴ └───────────┘ ┴
typ ┴ ┴ └──────────────┘ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴
55 (by simp [function.funext_iff, fintype.complete])
id └─────────────────┘ └──────────────┘
src └────┘└─────────────────┘└┘└──────────────┘┴
typ └────┘└─────────────────┘└┘└──────────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └───────────────────────────────────────────┘
56
57 instance decidable_forall_fintype [fintype α] {p : α → Prop} [decidable_pred p] :
id └─────┘ ┴ ┴ └────────────┘ ┴
src └─────┘ └────────────┘
typ └─────┘ ┴ ┴ └────────────┘ ┴
doc └─────┘
58 decidable (∀ a, p a) :=
id └───────┘ ┴ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴ ┴
59 decidable_of_iff (∀ a ∈ @univ α _, p a) (by simp)
id └──────────────┘ ┴ └──┘ ┴ ┴ ┴
src └──────────────┘ └──┘ └──┘
typ └──────────────┘ ┴ └──┘ ┴ ┴ ┴ └──┘
doc └──┘ └──┘
txt └──┘
par └──┘
st └───┘
60
61 instance decidable_exists_fintype [fintype α] {p : α → Prop} [decidable_pred p] :
id └─────┘ ┴ ┴ └────────────┘ ┴
src └─────┘ └────────────┘
typ └─────┘ ┴ ┴ └────────────┘ ┴
doc └─────┘
62 decidable (∃ a, p a) :=
id └───────┘ ┴ ┴┴ ┴ ┴
src └───────┘ ┴ ┴
typ └───────┘ ┴ ┴┴ ┴ ┴
63 decidable_of_iff (∃ a ∈ @univ α _, p a) (by simp)
id └──────────────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └──────────────┘ ┴ └──┘ ┴ └──┘
typ └──────────────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘
doc └──┘ └──┘
txt └──┘
par └──┘
st └───┘
64
65 instance decidable_eq_equiv_fintype [fintype α] [decidable_eq β] :
id └─────┘ ┴ └──────────┘ ┴
src └─────┘ └──────────┘
typ └─────┘ ┴ └──────────┘ ┴
doc └─────┘
66 decidable_eq (α ≃ β) :=
id └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴
doc ┴
67 λ a b, decidable_of_iff (a.1 = b.1) ⟨λ h, equiv.ext _ _ (congr_fun h), congr_arg _⟩
id ┴ ┴ └──────────────┘ ┴┴ ┴ ┴┴ ┴ └───────┘ └───────┘ ┴ └───────┘
src └──────────────┘ ┴ ┴ ┴ └───────┘ └───────┘ └───────┘
typ ┴ ┴ └──────────────┘ ┴┴ ┴ ┴┴ ┴ └───────┘ └───────┘ ┴ └───────┘
68
69 instance decidable_injective_fintype [fintype α] [decidable_eq α] [decidable_eq β] :
id └─────┘ ┴ └──────────┘ ┴ └──────────┘ ┴
src └─────┘ └──────────┘ └──────────┘
typ └─────┘ ┴ └──────────┘ ┴ └──────────┘ ┴
doc └─────┘
70 decidable_pred (injective : (α → β) → Prop) := λ x, by unfold injective; apply_instance
id └────────────┘ └───────┘ ┴ ┴ ┴ ┴
src └────────────┘ └───────┘ └──────────────┘ └──────────────
typ └────────────┘ └───────┘ ┴ ┴ ┴ ┴ └──────────────┘ └──────────────
doc └──────────────┘ └──────────────
txt └──────────────┘ └──────────────
par └──────────────┘ └──────────────
pid └────────┘ └
st └─────────────────────────────────
71
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
72 instance decidable_surjective_fintype [fintype α] [fintype β] [decidable_eq β] :
id └─────┘ ┴ └─────┘ ┴ └──────────┘ ┴
src └─────┘ └─────┘ └──────────┘
typ └─────┘ ┴ └─────┘ ┴ └──────────┘ ┴
doc └─────┘ └─────┘
73 decidable_pred (surjective : (α → β) → Prop) := λ x, by unfold surjective; apply_instance
id └────────────┘ └────────┘ ┴ ┴ ┴ ┴
src └────────────┘ └────────┘ └───────────────┘ └──────────────
typ └────────────┘ └────────┘ ┴ ┴ ┴ ┴ └───────────────┘ └──────────────
doc └───────────────┘ └──────────────
txt └───────────────┘ └──────────────
par └───────────────┘ └──────────────
pid └─────────┘ └
st └──────────────────────────────────
74
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
75 instance decidable_bijective_fintype [fintype α] [decidable_eq α] [fintype β] [decidable_eq β] :
id └─────┘ ┴ └──────────┘ ┴ └─────┘ ┴ └──────────┘ ┴
src └─────┘ └──────────┘ └─────┘ └──────────┘
typ └─────┘ ┴ └──────────┘ ┴ └─────┘ ┴ └──────────┘ ┴
doc └─────┘ └─────┘
76 decidable_pred (bijective : (α → β) → Prop) := λ x, by unfold bijective; apply_instance
id └────────────┘ └───────┘ ┴ ┴ ┴ ┴
src └────────────┘ └───────┘ └──────────────┘ └──────────────
typ └────────────┘ └───────┘ ┴ ┴ ┴ ┴ └──────────────┘ └──────────────
doc └──────────────┘ └──────────────
txt └──────────────┘ └──────────────
par └──────────────┘ └──────────────
pid └────────┘ └
st └─────────────────────────────────
77
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
78 instance decidable_left_inverse_fintype [fintype α] [decidable_eq α] (f : α → β) (g : β → α) :
id └─────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──────────┘
typ └─────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘
79 decidable (function.right_inverse f g) :=
id └───────┘ └────────────────────┘ ┴ ┴
src └───────┘ └────────────────────┘
typ └───────┘ └────────────────────┘ ┴ ┴
80 show decidable (∀ x, g (f x) = x), by apply_instance
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ └──────────────
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────
doc └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
81
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
82 instance decidable_right_inverse_fintype [fintype β] [decidable_eq β] (f : α → β) (g : β → α) :
id └─────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──────────┘
typ └─────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘
83 decidable (function.left_inverse f g) :=
id └───────┘ └───────────────────┘ ┴ ┴
src └───────┘ └───────────────────┘
typ └───────┘ └───────────────────┘ ┴ ┴
84 show decidable (∀ x, f (g x) = x), by apply_instance
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ └──────────────
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────────
doc └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
85
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
86 /-- Construct a proof of `fintype α` from a universal multiset -/
87 def of_multiset [decidable_eq α] (s : multiset α)
id └──────────┘ ┴ └──────┘ ┴
src └──────────┘ └──────┘
typ └──────────┘ ┴ └──────┘ ┴
doc └──────┘
88 (H : ∀ x : α, x ∈ s) : fintype α :=
id ┴ ┴ ┴ ┴ └─────┘ ┴
src ┴ └─────┘
typ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
89 ⟨s.to_finset, by simpa using H⟩
id ┴└────────┘ ┴
src └────────┘ └──────────┘
typ ┴└────────┘ └──────────┘┴
doc └────────┘ └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └────────────┘
90
91 /-- Construct a proof of `fintype α` from a universal list -/
92 def of_list [decidable_eq α] (l : list α)
id └──────────┘ ┴ └──┘ ┴
src └──────────┘ └──┘
typ └──────────┘ ┴ └──┘ ┴
93 (H : ∀ x : α, x ∈ l) : fintype α :=
id ┴ ┴ ┴ ┴ └─────┘ ┴
src ┴ └─────┘
typ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
94 ⟨l.to_finset, by simpa using H⟩
id ┴└────────┘ ┴
src └────────┘ └──────────┘
typ ┴└────────┘ └──────────┘┴
doc └────────┘ └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └────────────┘
95
96 theorem exists_univ_list (α) [fintype α] :
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
doc └─────┘
97 ∃ l : list α, l.nodup ∧ ∀ x : α, x ∈ l :=
id ┴ └──┘ ┴┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ └────┘ ┴ ┴
typ ┴ └──┘ ┴┴ ┴└────┘ ┴ ┴ ┴ ┴ ┴
doc └────┘
98 let ⟨l, e⟩ := quotient.exists_rep (@univ α _).1 in
id └─┘ └─────────────────┘ └──┘ ┴ ┴
src └─────────────────┘ └──┘ ┴
typ └─┘ └─────────────────┘ └──┘ ┴ ┴
doc └──┘
99 by have := and.intro univ.2 mem_univ_val;
id └───────┘ └──┘ └──────────┘
src └──────┘└───────┘┴└──┘└─┘└──────────┘
typ └──────┘└───────┘┴└──┘└─┘└──────────┘
doc └──────┘ ┴└──┘└─┘
txt └──────┘ ┴ └─┘
par └──────┘ ┴ └─┘
pid └───┘└─┘ ┴ └─┘
st └───────────────────────────────────────
100 exact ⟨_, by rwa ← e at this⟩
id ┴
src └────┘ └─┘ ┴└────┘ └──────┘└─
typ └────┘ └─┘ ┴└────┘┴└──────┘└─
doc └────┘ └─┘ ┴└────┘ └──────┘└─
txt └────┘ └─┘ ┴└────┘ └──────┘└─
par └────┘ └─┘ ┴└────┘ └──────┘└─
pid ┴ └─┘ └─────┘ └───────┘└
st ──────────────┘└──────────────┘└─
101
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
102 /-- `card α` is the number of elements in `α`, defined when `α` is a fintype. -/
103 def card (α) [fintype α] : ℕ := (@univ α _).card
id └─────┘ ┴ ┴ └──┘ ┴ └──┘
src └─────┘ ┴ └──┘ └──┘
typ └─────┘ ┴ ┴ └──┘ ┴ └──┘
doc └─────┘ └──┘ └──┘
104
105 /-- If `l` lists all the elements of `α` without duplicates, then `α ≃ fin (l.length)`. -/
106 def equiv_fin_of_forall_mem_list {α} [decidable_eq α]
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
107 {l : list α} (h : ∀ x:α, x ∈ l) (nd : l.nodup) : α ≃ fin (l.length) :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴└────┘ ┴ ┴ └─┘ ┴└─────┘
src └──┘ ┴ └────┘ ┴ └─┘ └─────┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴└────┘ ┴ ┴ └─┘ ┴└─────┘
doc └────┘ ┴
108 ⟨λ a, ⟨_, list.index_of_lt_length.2 (h a)⟩,
id ┴ └─────────────────────┘┴ ┴ ┴
src └─────────────────────┘┴
typ ┴ └─────────────────────┘┴ ┴ ┴
109 λ i, l.nth_le i.1 i.2,
id ┴ ┴└─────┘ ┴┴ ┴┴
src └─────┘ ┴ ┴
typ ┴ ┴└─────┘ ┴┴ ┴┴
110 λ a, by simp,
id ┴
src └──┘
typ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
111 λ ⟨i, h⟩, fin.eq_of_veq $ list.nodup_iff_nth_le_inj.1 nd _ _
id ┴ ┴ └───────────┘ └───────────────────────┘┴ └┘
src └───────────┘ └───────────────────────┘┴
typ ┴ ┴ └───────────┘ └───────────────────────┘┴ └┘
112 (list.index_of_lt_length.2 (list.nth_le_mem _ _ _)) h $ by simp⟩
id └─────────────────────┘┴ └─────────────┘
src └─────────────────────┘┴ └─────────────┘ └──┘
typ └─────────────────────┘┴ └─────────────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
113
114 /-- There is (computably) a bijection between `α` and `fin n` where
115 `n = card α`. Since it is not unique, and depends on which permutation
116 of the universe list is used, the bijection is wrapped in `trunc` to
117 preserve computability. -/
118 def equiv_fin (α) [fintype α] [decidable_eq α] : trunc (α ≃ fin (card α)) :=
id └─────┘ ┴ └──────────┘ ┴ └───┘ ┴ ┴ └─┘ └──┘ ┴
src └─────┘ └──────────┘ └───┘ ┴ └─┘ └──┘
typ └─────┘ ┴ └──────────┘ ┴ └───┘ ┴ ┴ └─┘ └──┘ ┴
doc └─────┘ └───┘ ┴ └──┘
119 by unfold card finset.card; exact
src └─────────────────────┘ └────┘
typ └─────────────────────┘ └────┘
doc └─────────────────────┘ └────┘
txt └─────────────────────┘ └────┘
par └─────────────────────┘ └────┘
pid └───────────────┘ ┴
st └───────────────────────────────
120 quot.rec_on_subsingleton (@univ α _).1
id └──────────────────────┘
src └──────────────────────┘┴ ┴ └─────
typ └──────────────────────┘┴ ┴ └─────
doc ┴ ┴ └─────
txt ┴ ┴ └─────
par ┴ ┴ └─────
pid ┴ ┴ └─────
st ───────────────────────────────────────
121 (λ l (h : ∀ x:α, x ∈ l) (nd : l.nodup), trunc.mk (equiv_fin_of_forall_mem_list h nd))
id ┴ ┴ └────┘ └──────┘ └──────────────────────────┘
src ─┘ └──────┘ └─┘ ┴ ┴┴┴ └──────┘ └────┘└─┘└──────┘┴ └──────────────────────────┘┴ ┴ └──
typ ─┘ └──────┘ └─┘┴ ┴ ┴┴┴ └──────┘ └────┘└─┘└──────┘┴ └──────────────────────────┘┴ ┴ └──
doc ─┘ └──────┘ └─┘ ┴ ┴ ┴ └──────┘ └────┘└─┘└──────┘┴ └──────────────────────────┘┴ ┴ └──
txt ─┘ └──────┘ └─┘ ┴ ┴ ┴ └──────┘ └─┘ ┴ ┴ ┴ └──
par ─┘ └──────┘ └─┘ ┴ ┴ ┴ └──────┘ └─┘ ┴ ┴ ┴ └──
pid ─┘ └──────┘ └─┘ ┴ ┴ ┴ └──────┘ └─┘ ┴ ┴ ┴ └──
st ────────────────────────────────────────────────────────────────────────────────────────
122 mem_univ_val univ.2
id └──────────┘ └──┘
src ─┘└──────────┘┴└──┘└──
typ ─┘└──────────┘┴└──┘└──
doc ─┘ ┴└──┘└──
txt ─┘ ┴ └──
par ─┘ ┴ └──
pid ─┘ ┴ └──
st ──────────────────────
123
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
124 theorem exists_equiv_fin (α) [fintype α] : ∃ n, nonempty (α ≃ fin n) :=
id └─────┘ ┴ ┴ ┴┴ └──────┘ ┴ ┴ └─┘ ┴
src └─────┘ ┴ ┴ └──────┘ ┴ └─┘
typ └─────┘ ┴ ┴ ┴┴ └──────┘ ┴ ┴ └─┘ ┴
doc └─────┘ ┴
125 by haveI := classical.dec_eq α; exact ⟨card α, nonempty_of_trunc (equiv_fin α)⟩
id └──────────────┘ ┴ └──┘ └───────────────┘ └───────┘ ┴
src └───────┘└──────────────┘┴ └────┘ └──┘┴ └┘└───────────────┘┴ └───────┘┴ └──
typ └───────┘└──────────────┘┴┴ └────┘ └──┘┴ └┘└───────────────┘┴ └───────┘┴┴└──
doc └───────┘ ┴ └────┘ └──┘┴ └┘ ┴ └───────┘┴ └──
txt └───────┘ ┴ └────┘ ┴ └┘ ┴ ┴ └──
par └───────┘ ┴ └────┘ ┴ └┘ ┴ ┴ └──
pid ┴└─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘└
st └─────────────────────────────────────────────────────────────────────────────
126
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
127 instance (α : Type*) : subsingleton (fintype α) :=
id └──────────┘ └─────┘ ┴
src └──────────┘ └─────┘
typ └──────────┘ └─────┘ ┴
doc └─────┘
128 ⟨λ ⟨s₁, h₁⟩ ⟨s₂, h₂⟩, by congr; simp [finset.ext, h₁, h₂]⟩
id ┴ ┴ └────────┘ └┘ └┘
src └───┘ └────┘└────────┘└┘ └┘ ┴
typ ┴ ┴ └───┘ └────┘└────────┘└┘└┘└┘└┘┴
doc └────┘ └┘ └┘ ┴
txt └───┘ └────┘ └┘ └┘ ┴
par └───┘ └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st └───────────────────────────────┘
129
130 protected def subtype {p : α → Prop} (s : finset α)
id ┴ └────┘ ┴
src └────┘
typ ┴ └────┘ ┴
doc └────┘
131 (H : ∀ x : α, x ∈ s ↔ p x) : fintype {x // p x} :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴┴ ┴ ┴
src ┴ ┴ └─────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴┴ ┴ ┴
doc └─────┘
132 ⟨⟨multiset.pmap subtype.mk s.1 (λ x, (H x).1),
id └───────────┘ └────────┘ ┴┴ ┴ ┴ ┴ ┴
src └───────────┘ └────────┘ ┴ ┴
typ └───────────┘ └────────┘ ┴┴ ┴ ┴ ┴ ┴
doc └───────────┘
133 multiset.nodup_pmap (λ a _ b _, congr_arg subtype.val) s.2⟩,
id └─────────────────┘ ┴ ┴ ┴ ┴ └───────┘ └─────────┘ ┴┴
src └─────────────────┘ └───────┘ └─────────┘ ┴
typ └─────────────────┘ ┴ ┴ ┴ ┴ └───────┘ └─────────┘ ┴┴
134 λ ⟨x, px⟩, multiset.mem_pmap.2 ⟨x, (H x).2 px, rfl⟩⟩
id ┴┴ └┘ └───────────────┘┴ ┴ ┴ └─┘
src └───────────────┘┴ ┴ └─┘
typ ┴┴ └┘ └───────────────┘┴ ┴ ┴ └─┘
135
136 theorem subtype_card {p : α → Prop} (s : finset α)
id ┴ └────┘ ┴
src └────┘
typ ┴ └────┘ ┴
doc └────┘
137 (H : ∀ x : α, x ∈ s ↔ p x) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
138 @card {x // p x} (fintype.subtype s H) = s.card :=
id └──┘ ┴┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴└───┘
src └──┘ ┴ └─────────────┘ ┴ └───┘
typ └──┘ ┴┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴└───┘
doc └──┘ └───┘
139 multiset.card_pmap _ _ _
id └────────────────┘
src └────────────────┘
typ └────────────────┘
140
141 theorem card_of_subtype {p : α → Prop} (s : finset α)
id ┴ └────┘ ┴
src └────┘
typ ┴ └────┘ ┴
doc └────┘
142 (H : ∀ x : α, x ∈ s ↔ p x) [fintype {x // p x}] :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴┴ ┴ ┴
src ┴ ┴ └─────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴┴ ┴ ┴
doc └─────┘
143 card {x // p x} = s.card :=
id └──┘ ┴┴ ┴ ┴ ┴ ┴└───┘
src └──┘ ┴ ┴ └───┘
typ └──┘ ┴┴ ┴ ┴ ┴ ┴└───┘
doc └──┘ └───┘
144 by rw ← subtype_card s H; congr
id └──────────┘ ┴ ┴
src └───┘└──────────┘┴ ┴ └─────
typ └───┘└──────────┘┴┴┴┴ └─────
doc └───┘ ┴ ┴
txt └───┘ ┴ ┴ └─────
par └───┘ ┴ ┴ └─────
pid └─┘ ┴ ┴ └
st └─────────────────────────────
145
src ┘
typ ┘
txt ┘
par ┘
pid ┘
st ┘
146 /-- Construct a fintype from a finset with the same elements. -/
147 def of_finset {p : set α} (s : finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) : fintype p :=
id └─┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src └─┘ └────┘ ┴ ┴ ┴ └─────┘
typ └─┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └────┘ └─────┘
148 fintype.subtype s H
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
149
150 @[simp] theorem card_of_finset {p : set α} (s : finset α) (H : ∀ x, x ∈ s ↔ x ∈ p) :
id └─┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └────┘ ┴ ┴ ┴
typ └─┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └────┘
151 @fintype.card p (of_finset s H) = s.card :=
id └──────────┘ ┴ └───────┘ ┴ ┴ ┴ ┴└───┘
src └──────────┘ └───────┘ ┴ └───┘
typ └──────────┘ ┴ └───────┘ ┴ ┴ ┴ ┴└───┘
doc └──────────┘ └───────┘ └───┘
152 fintype.subtype_card s H
id └──────────────────┘ ┴ ┴
src └──────────────────┘
typ └──────────────────┘ ┴ ┴
153
154 theorem card_of_finset' {p : set α} (s : finset α)
id └─┘ ┴ └────┘ ┴
src └─┘ └────┘
typ └─┘ ┴ └────┘ ┴
doc └────┘
155 (H : ∀ x, x ∈ s ↔ x ∈ p) [fintype p] : fintype.card p = s.card :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └──────────┘ ┴ ┴ ┴└───┘
src ┴ ┴ ┴ └─────┘ └──────────┘ ┴ └───┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └──────────┘ ┴ ┴ ┴└───┘
doc └─────┘ └──────────┘ └───┘
156 by rw ← card_of_finset s H; congr
id └────────────┘ ┴ ┴
src └───┘└────────────┘┴ ┴ └─────
typ └───┘└────────────┘┴┴┴┴ └─────
doc └───┘ ┴ ┴
txt └───┘ ┴ ┴ └─────
par └───┘ ┴ ┴ └─────
pid └─┘ ┴ ┴ └
st └───────────────────────────────
157
src ┘
typ ┘
txt ┘
par ┘
pid ┘
st ┘
158 /-- If `f : α → β` is a bijection and `α` is a fintype, then `β` is also a fintype. -/
159 def of_bijective [fintype α] (f : α → β) (H : function.bijective f) : fintype β :=
id └─────┘ ┴ ┴ ┴ └────────────────┘ ┴ └─────┘ ┴
src └─────┘ └────────────────┘ └─────┘
typ └─────┘ ┴ ┴ ┴ └────────────────┘ ┴ └─────┘ ┴
doc └─────┘ └─────┘
160 ⟨univ.map ⟨f, H.1⟩,
id └──┘└──┘ ┴ ┴┴
src └──┘└──┘ ┴
typ └──┘└──┘ ┴ ┴┴
doc └──┘
161 λ b, let ⟨a, e⟩ := H.2 b in e ▸ mem_map_of_mem _ (mem_univ _)⟩
id ┴ └─┘ ┴ ┴┴ ┴ ┴ └────────────┘ └──────┘
src ┴ ┴ └────────────┘ └──────┘
typ ┴ └─┘ ┴ ┴┴ ┴ ┴ └────────────┘ └──────┘
162
163 /-- If `f : α → β` is a surjection and `α` is a fintype, then `β` is also a fintype. -/
164 def of_surjective [fintype α] [decidable_eq β] (f : α → β) (H : function.surjective f) : fintype β :=
id └─────┘ ┴ └──────────┘ ┴ ┴ ┴ └─────────────────┘ ┴ └─────┘ ┴
src └─────┘ └──────────┘ └─────────────────┘ └─────┘
typ └─────┘ ┴ └──────────┘ ┴ ┴ ┴ └─────────────────┘ ┴ └─────┘ ┴
doc └─────┘ └─────┘
165 ⟨univ.image f, λ b, let ⟨a, e⟩ := H b in e ▸ mem_image_of_mem _ (mem_univ _)⟩
id └──┘└────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └──────────────┘ └──────┘
src └──┘└────┘ ┴ └──────────────┘ └──────┘
typ └──┘└────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └──────────────┘ └──────┘
doc └──┘└────┘
166
167 noncomputable def of_injective [fintype β] (f : α → β) (H : function.injective f) : fintype α :=
id └─────┘ ┴ ┴ ┴ └────────────────┘ ┴ └─────┘ ┴
src └─────┘ └────────────────┘ └─────┘
typ └─────┘ ┴ ┴ ┴ └────────────────┘ ┴ └─────┘ ┴
doc └─────┘ └─────┘
168 by letI := classical.dec; exact
id └───────────┘
src └──────┘└───────────┘ └────┘
typ └──────┘└───────────┘ └────┘
doc └──────┘ └────┘
txt └──────┘ └────┘
par └──────┘ └────┘
pid ┴└─┘ ┴
st └─────────────────────────────
169 if hα : nonempty α then by letI := classical.inhabited_of_nonempty hα;
id └┘ └──────┘ ┴ └─────────────────────────────┘ └┘
src └┘└────┘└──────┘┴ └────┘ ┴└──────┘└─────────────────────────────┘┴ └─
typ └┘└────┘└──────┘┴┴└────┘ ┴└──────┘└─────────────────────────────┘┴└┘└─
doc └────┘ ┴ └────┘ ┴└──────┘ ┴ └─
txt └────┘ ┴ └────┘ ┴└──────┘ ┴ └─
par └────┘ ┴ └────┘ ┴└──────┘ ┴ └─
pid └────┘ ┴ └────┘ └───────┘ ┴ └─
st ─────────────────────────┘└────────────────────────────────────────────
170 exact of_surjective (inv_fun f) (inv_fun_surjective H)
id └───────────┘ └─────┘ ┴ └────────────────┘ ┴
src ───────┘└───────────┘┴ └─────┘┴ └┘ └────────────────┘┴ └─
typ ───────┘└───────────┘┴ └─────┘┴┴└┘ └────────────────┘┴┴└─
doc ───────┘└───────────┘┴ └─────┘┴ └┘ ┴ └─
txt ───────┘ ┴ ┴ └┘ ┴ └─
par ───────┘ ┴ ┴ └┘ ┴ └─
pid ───────┘ ┴ ┴ └┘ ┴ └─
st ────────────────────────────────────────────────────────┘
171 else ⟨∅, λ x, (hα ⟨x⟩).elim⟩
id ┴┴
src ────┘┴┴└┘ └──┘ ┴ └────────
typ ────┘┴┴└┘ └──┘ ┴ └────────
doc ────┘ └┘ └──┘ ┴ └────────
txt ────┘ └┘ └──┘ ┴ └────────
par ────┘ └┘ └──┘ ┴ └────────
pid ────┘ └┘ └──┘ ┴ └──────┘└
st └────────────────────────────
172
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
173 /-- If `f : α ≃ β` and `α` is a fintype, then `β` is also a fintype. -/
174 def of_equiv (α : Type*) [fintype α] (f : α ≃ β) : fintype β := of_bijective _ f.bijective
id └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └──────────┘ ┴└────────┘
src └─────┘ ┴ └─────┘ └──────────┘ └────────┘
typ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └──────────┘ ┴└────────┘
doc └─────┘ ┴ └─────┘ └──────────┘
175
176 theorem of_equiv_card [fintype α] (f : α ≃ β) :
id └─────┘ ┴ ┴ ┴ ┴
src └─────┘ ┴
typ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘ ┴
177 @card β (of_equiv α f) = card α :=
id └──┘ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴
src └──┘ └──────┘ ┴ └──┘
typ └──┘ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴
doc └──┘ └──────┘ └──┘
178 multiset.card_map _ _
id └───────────────┘
src └───────────────┘
typ └───────────────┘
179
180 theorem card_congr {α β} [fintype α] [fintype β] (f : α ≃ β) : card α = card β :=
id └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src └─────┘ └─────┘ ┴ └──┘ ┴ └──┘
typ └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └─────┘ └─────┘ ┴ └──┘ └──┘
181 by rw ← of_equiv_card f; congr
id └───────────┘ ┴
src └───┘└───────────┘┴ └─────
typ └───┘└───────────┘┴┴ └─────
doc └───┘ ┴
txt └───┘ ┴ └─────
par └───┘ ┴ └─────
pid └─┘ ┴ └
st └────────────────────────────
182
src ┘
typ ┘
txt ┘
par ┘
pid ┘
st ┘
183 theorem card_eq {α β} [F : fintype α] [G : fintype β] : card α = card β ↔ nonempty (α ≃ β) :=
id └─────┘ ┴ └─────┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └──────┘ ┴ ┴ ┴
src └─────┘ └─────┘ └──┘ ┴ └──┘ ┴ └──────┘ ┴
typ └─────┘ ┴ └─────┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └──────┘ ┴ ┴ ┴
doc └─────┘ └─────┘ └──┘ └──┘ ┴
184 ⟨λ h, ⟨by classical;
id ┴
src └───────┘
typ ┴ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
st └───────────
185 calc α ≃ fin (card α) : trunc.out (equiv_fin α)
id └──┘ └─┘ └──┘ ┴
src └──┘ └─┘ └──┘
typ └──┘ └─┘ └──┘ ┴
doc └──┘ └──┘
st ──────────────────────────────────────────────────
186 ... ≃ fin (card β) : by rw h
id ┴
src └─┘ └
typ └─┘┴└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st ───────────────────────────┘└─────
187 ... ≃ β : (trunc.out (equiv_fin β)).symm⟩,
id └───────┘ └───────┘ ┴ └──┘
src ────┘ └───────┘ └───────┘ └──┘
typ ────┘ └───────┘ └───────┘ ┴ └──┘
doc ────┘ └───────┘ └───────┘
txt ────┘
par ────┘
pid ────┘
st ────┘└─────────────────────────────────────┘
188 λ ⟨f⟩, card_congr f⟩
id ┴┴ └────────┘
src └────────┘
typ ┴┴ └────────┘
189
190 def of_subsingleton (a : α) [subsingleton α] : fintype α :=
id ┴ └──────────┘ ┴ └─────┘ ┴
src └──────────┘ └─────┘
typ ┴ └──────────┘ ┴ └─────┘ ┴
doc └─────┘
191 ⟨finset.singleton a, λ b, finset.mem_singleton.2 (subsingleton.elim _ _)⟩
id └──────────────┘ ┴ ┴ └──────────────────┘┴ └───────────────┘
src └──────────────┘ └──────────────────┘┴ └───────────────┘
typ └──────────────┘ ┴ ┴ └──────────────────┘┴ └───────────────┘
doc └──────────────┘
192
193 @[simp] theorem univ_of_subsingleton (a : α) [subsingleton α] :
id ┴ └──────────┘ ┴
src └──────────┘
typ ┴ └──────────┘ ┴
doc └──┘
194 @univ _ (of_subsingleton a) = finset.singleton a := rfl
id └──┘ └─────────────┘ ┴ ┴ └──────────────┘ ┴ └─┘
src └──┘ └─────────────┘ ┴ └──────────────┘ └─┘
typ └──┘ └─────────────┘ ┴ ┴ └──────────────┘ ┴ └─┘
doc └──┘ └──────────────┘
195
196 @[simp] theorem card_of_subsingleton (a : α) [subsingleton α] :
id ┴ └──────────┘ ┴
src └──────────┘
typ ┴ └──────────┘ ┴
doc └──┘
197 @fintype.card _ (of_subsingleton a) = 1 := rfl
id └──────────┘ └─────────────┘ ┴ ┴ └─┘
src └──────────┘ └─────────────┘ ┴ └─┘
typ └──────────┘ └─────────────┘ ┴ ┴ └─┘
doc └──────────┘
198
199 lemma card_eq_sum_ones {α} [fintype α] : fintype.card α = (finset.univ : finset α).sum (λ _, 1) :=
id └─────┘ ┴ └──────────┘ ┴ ┴ └─────────┘ └────┘ ┴ └─┘ ┴
src └─────┘ └──────────┘ ┴ └─────────┘ └────┘ └─┘
typ └─────┘ ┴ └──────────┘ ┴ ┴ └─────────┘ └────┘ ┴ └─┘ ┴
doc └─────┘ └──────────┘ └─────────┘ └────┘
200 finset.card_eq_sum_ones _
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
201
202 end fintype
203
204 namespace set
205
206 /-- Construct a finset enumerating a set `s`, given a `fintype` instance. -/
207 def to_finset (s : set α) [fintype s] : finset α :=
id └─┘ ┴ └─────┘ ┴ └────┘ ┴
src └─┘ └─────┘ └────┘
typ └─┘ ┴ └─────┘ ┴ └────┘ ┴
doc └─────┘ └────┘
208 ⟨(@finset.univ s _).1.map subtype.val,
id └─────────┘ ┴ ┴ └─┘ └─────────┘
src └─────────┘ ┴ └─┘ └─────────┘
typ └─────────┘ ┴ ┴ └─┘ └─────────┘
doc └─────────┘ └─┘
209 multiset.nodup_map (λ a b, subtype.eq) finset.univ.2⟩
id └────────────────┘ ┴ ┴ └────────┘ └─────────┘┴
src └────────────────┘ └────────┘ └─────────┘┴
typ └────────────────┘ ┴ ┴ └────────┘ └─────────┘┴
doc └─────────┘
210
211 @[simp] theorem mem_to_finset {s : set α} [fintype s] {a : α} : a ∈ s.to_finset ↔ a ∈ s :=
id └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴└────────┘ ┴ ┴ ┴ ┴
src └─┘ └─────┘ ┴ └────────┘ ┴ ┴
typ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴└────────┘ ┴ ┴ ┴ ┴
doc └──┘ └─────┘ └────────┘
212 by simp [to_finset]
id └───────┘
src └────┘└───────┘└─
typ └────┘└───────┘└─
doc └────┘└───────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └─────────────────
213
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
214 @[simp] theorem mem_to_finset_val {s : set α} [fintype s] {a : α} : a ∈ s.to_finset.1 ↔ a ∈ s :=
id └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴└────────┘┴ ┴ ┴ ┴ ┴
src └─┘ └─────┘ ┴ └────────┘┴ ┴ ┴
typ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴└────────┘┴ ┴ ┴ ┴ ┴
doc └──┘ └─────┘ └────────┘
215 mem_to_finset
id └───────────┘
src └───────────┘
typ └───────────┘
216
217 end set
218
219 lemma finset.card_univ [fintype α] : (finset.univ : finset α).card = fintype.card α :=
id └─────┘ ┴ └─────────┘ └────┘ ┴ └──┘ ┴ └──────────┘ ┴
src └─────┘ └─────────┘ └────┘ └──┘ ┴ └──────────┘
typ └─────┘ ┴ └─────────┘ └────┘ ┴ └──┘ ┴ └──────────┘ ┴
doc └─────┘ └─────────┘ └────┘ └──┘ └──────────┘
220 rfl
id └─┘
src └─┘
typ └─┘
221
222 lemma finset.card_univ_diff [fintype α] [decidable_eq α] (s : finset α) :
id └─────┘ ┴ └──────────┘ ┴ └────┘ ┴
src └─────┘ └──────────┘ └────┘
typ └─────┘ ┴ └──────────┘ ┴ └────┘ ┴
doc └─────┘ └────┘
223 (finset.univ \ s).card = fintype.card α - s.card :=
id └─────────┘ ┴ ┴ └──┘ ┴ └──────────┘ ┴ ┴ ┴└───┘
src └─────────┘ ┴ └──┘ ┴ └──────────┘ ┴ └───┘
typ └─────────┘ ┴ ┴ └──┘ ┴ └──────────┘ ┴ ┴ ┴└───┘
doc └─────────┘ └──┘ └──────────┘ └───┘
224 finset.card_sdiff (subset_univ s)
id └───────────────┘ └─────────┘ ┴
src └───────────────┘ └─────────┘
typ └───────────────┘ └─────────┘ ┴
225
226 instance (n : ℕ) : fintype (fin n) :=
id ┴ └─────┘ └─┘ ┴
src ┴ └─────┘ └─┘
typ ┴ └─────┘ └─┘ ┴
doc └─────┘
227 ⟨⟨list.fin_range n, list.nodup_fin_range n⟩, list.mem_fin_range⟩
id └────────────┘ ┴ └──────────────────┘ ┴ └────────────────┘
src └────────────┘ └──────────────────┘ └────────────────┘
typ └────────────┘ ┴ └──────────────────┘ ┴ └────────────────┘
doc └────────────┘
228
229 @[simp] theorem fintype.card_fin (n : ℕ) : fintype.card (fin n) = n :=
id ┴ └──────────┘ └─┘ ┴ ┴ ┴
src ┴ └──────────┘ └─┘ ┴
typ ┴ └──────────┘ └─┘ ┴ ┴ ┴
doc └──┘ └──────────┘
230 list.length_fin_range n
id └───────────────────┘ ┴
src └───────────────────┘
typ └───────────────────┘ ┴
231
232 lemma fin.univ_succ (n : ℕ) :
id ┴
src ┴
typ ┴
233 (univ : finset (fin $ n+1)) = insert 0 (univ.image fin.succ) :=
id └──┘ └────┘ └─┘ ┴┴ ┴ └────┘ └──┘└────┘ └──────┘
src └──┘ └────┘ └─┘ ┴ ┴ └────┘ └──┘└────┘ └──────┘
typ └──┘ └────┘ └─┘ ┴┴ ┴ └────┘ └──┘└────┘ └──────┘
doc └──┘ └────┘ └──┘└────┘
234 begin
st └─────
235 ext m,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
236 simp only [mem_univ, mem_insert, true_iff, mem_image, exists_prop],
id └──────┘ └────────┘ └──────┘ └───────┘ └─────────┘
src └─────────┘└──────┘└┘└────────┘└┘└──────┘└┘└───────┘└┘└─────────┘┴
typ └─────────┘└──────┘└┘└────────┘└┘└──────┘└┘└───────┘└┘└─────────┘┴
doc └─────────┘ └┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴
st ───────────────────────────────────────────────────────────────────┘└─
237 exact fin.cases (or.inl rfl) (λ i, or.inr ⟨i, trivial, rfl⟩) m
id └───────┘ └────┘ └────┘ └─────┘ └─┘ ┴
src └────┘└───────┘┴ └────┘┴ └┘ └──┘└────┘┴ └┘└─────┘└┘└─┘└─┘ ┴
typ └────┘└───────┘┴ └────┘┴ └┘ └──┘└────┘┴ └┘└─────┘└┘└─┘└─┘┴┴
doc └────┘ ┴ ┴ └┘ └──┘ ┴ └┘ └┘ └─┘ ┴
txt └────┘ ┴ ┴ └┘ └──┘ ┴ └┘ └┘ └─┘ ┴
par └────┘ ┴ ┴ └┘ └──┘ ┴ └┘ └┘ └─┘ ┴
pid ┴ ┴ ┴ └┘ └──┘ ┴ └┘ └┘ └─┘ ┴
st ────────────────────────────────────────────────────────────────┘
238 end
st └─┘
239
240 theorem fin.prod_univ_succ [comm_monoid β] {n:ℕ} (f : fin n.succ → β) :
id └─────────┘ ┴ ┴ └─┘ ┴└───┘ ┴
src └─────────┘ ┴ └─┘ └───┘
typ └─────────┘ ┴ ┴ └─┘ ┴└───┘ ┴
241 univ.prod f = f 0 * univ.prod (λ i:fin n, f i.succ) :=
id └──┘└───┘ ┴ ┴ ┴ ┴ └──┘└───┘ └─┘ ┴ ┴ ┴└───┘
src └──┘└───┘ ┴ ┴ └──┘└───┘ └─┘ └───┘
typ └──┘└───┘ ┴ ┴ ┴ ┴ └──┘└───┘ └─┘ ┴ ┴ ┴└───┘
doc └──┘└───┘ └──┘└───┘
242 begin
st └─────
243 rw [fin.univ_succ, prod_insert, prod_image],
id └───────────┘ └─────────┘ └────────┘
src └──┘└───────────┘└┘└─────────┘└┘└────────┘┴
typ └──┘└───────────┘└┘└─────────┘└┘└────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ──────────────────┘└───────────┘└──────────┘└──
244 { intros x _ y _ hxy, exact fin.succ.inj hxy },
id └──────────┘ └─┘
src └────────────────┘ └────┘└──────────┘┴ ┴
typ └────────────────┘ └────┘└──────────┘┴└─┘┴
doc └────────────────┘ └────┘ ┴ ┴
txt └────────────────┘ └────┘ ┴ ┴
par └────────────────┘ └────┘ ┴ ┴
pid └──────────┘ ┴ ┴ ┴
st ───┘└────────────────┘└───────────────────────┘└┘└
245 { simpa using fin.succ_ne_zero }
id └──────────────┘
src └──────────┘└──────────────┘┴
typ └──────────┘└──────────────┘┴
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid ┴└────┘ ┴
st ────────────────────────────────┘└─
246 end
st ──┘
247
248 @[simp, to_additive] theorem fin.prod_univ_zero [comm_monoid β] (f : fin 0 → β) : univ.prod f = 1 := rfl
id └─────────┘ ┴ └─┘ ┴ └──┘└───┘ ┴ ┴ └─┘
src └─────────┘ └─┘ └──┘└───┘ ┴ └─┘
typ └─────────┘ ┴ └─┘ ┴ └──┘└───┘ ┴ ┴ └─┘
doc └──┘ └─────────┘ └──┘└───┘
249
250 theorem fin.sum_univ_succ [add_comm_monoid β] {n:ℕ} (f : fin n.succ → β) :
id └─────────────┘ ┴ ┴ └─┘ ┴└───┘ ┴
src └─────────────┘ ┴ └─┘ └───┘
typ └─────────────┘ ┴ ┴ └─┘ ┴└───┘ ┴
251 univ.sum f = f 0 + univ.sum (λ i:fin n, f i.succ) :=
id └──┘└──┘ ┴ ┴ ┴ ┴ └──┘└──┘ └─┘ ┴ ┴ ┴└───┘
src └──┘└──┘ ┴ ┴ └──┘└──┘ └─┘ └───┘
typ └──┘└──┘ ┴ ┴ ┴ ┴ └──┘└──┘ └─┘ ┴ ┴ ┴└───┘
doc └──┘ └──┘
252 by apply @fin.prod_univ_succ (multiplicative β)
id └────────────────┘ └────────────┘ ┴
src └────┘ └────────────────┘┴ └────────────┘┴ └─
typ └────┘ └────────────────┘┴ └────────────┘┴┴└─
doc └────┘ ┴ ┴ └─
txt └────┘ ┴ ┴ └─
par └────┘ ┴ ┴ └─
pid ┴ ┴ ┴ ┴└
st └─────────────────────────────────────────────
253
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
254 attribute [to_additive] fin.prod_univ_succ
id └────────────────┘
src └────────────────┘
typ └────────────────┘
doc └─────────┘
255
256 @[instance, priority 10] def unique.fintype {α : Type*} [unique α] : fintype α :=
id └────┘ ┴ └─────┘ ┴
src └────┘ └─────┘
typ └────┘ ┴ └─────┘ ┴
doc └─────┘
257 ⟨finset.singleton (default α), λ x, by rw [unique.eq_default x]; simp⟩
id └──────────────┘ └─────┘ ┴ ┴ └───────────────┘ ┴
src └──────────────┘ └─────┘ └──┘└───────────────┘┴ ┴ └──┘
typ └──────────────┘ └─────┘ ┴ ┴ └──┘└───────────────┘┴┴┴ └──┘
doc └──────────────┘ └──┘ ┴ ┴ └──┘
txt └──┘ ┴ ┴ └──┘
par └──┘ ┴ ┴ └──┘
pid └┘ ┴ ┴
st └──────────────────────┘┴└────┘
258
259 @[simp] lemma univ_unique {α : Type*} [unique α] [f : fintype α] : @finset.univ α _ = {default α} :=
id └────┘ ┴ └─────┘ ┴ └─────────┘ ┴ ┴ ┴└─────┘ ┴
src └────┘ └─────┘ └─────────┘ ┴ ┴└─────┘
typ └────┘ ┴ └─────┘ ┴ └─────────┘ ┴ ┴ ┴└─────┘ ┴
doc └──┘ └─────┘ └─────────┘
260 by rw [subsingleton.elim f (@unique.fintype α _)]; refl
id └───────────────┘ ┴ └────────────┘ ┴
src └──┘└───────────────┘┴ ┴ └────────────┘┴ └──┘ └────
typ └──┘└───────────────┘┴┴┴ └────────────┘┴┴└──┘ └────
doc └──┘ ┴ ┴ ┴ └──┘ └────
txt └──┘ ┴ ┴ ┴ └──┘ └────
par └──┘ ┴ ┴ ┴ └──┘ └────
pid └┘ ┴ ┴ ┴ └──┘ └
st └────────────────────────────────────────────┘┴└──────
261
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
262 instance : fintype empty := ⟨∅, empty.rec _⟩
id └─────┘ └───┘ ┴ └───────┘
src └─────┘ └───┘ ┴ └───────┘
typ └─────┘ └───┘ ┴ └───────┘
doc └─────┘
263
264 @[simp] theorem fintype.univ_empty : @univ empty _ = ∅ := rfl
id └──┘ └───┘ ┴ ┴ └─┘
src └──┘ └───┘ ┴ ┴ └─┘
typ └──┘ └───┘ ┴ ┴ └─┘
doc └──┘ └──┘
265
266 @[simp] theorem fintype.card_empty : fintype.card empty = 0 := rfl
id └──────────┘ └───┘ ┴ └─┘
src └──────────┘ └───┘ ┴ └─┘
typ └──────────┘ └───┘ ┴ └─┘
doc └──┘ └──────────┘
267
268 instance : fintype pempty := ⟨∅, pempty.rec _⟩
id └─────┘ └────┘ ┴ └────────┘
src └─────┘ └────┘ ┴ └────────┘
typ └─────┘ └────┘ ┴ └────────┘
doc └─────┘ └────┘
269
270 @[simp] theorem fintype.univ_pempty : @univ pempty _ = ∅ := rfl
id └──┘ └────┘ ┴ ┴ └─┘
src └──┘ └────┘ ┴ ┴ └─┘
typ └──┘ └────┘ ┴ ┴ └─┘
doc └──┘ └──┘ └────┘
271
272 @[simp] theorem fintype.card_pempty : fintype.card pempty = 0 := rfl
id └──────────┘ └────┘ ┴ └─┘
src └──────────┘ └────┘ ┴ └─┘
typ └──────────┘ └────┘ ┴ └─┘
doc └──┘ └──────────┘ └────┘
273
274 instance : fintype unit := fintype.of_subsingleton ()
id └─────┘ └──┘ └─────────────────────┘ └┘
src └─────┘ └──┘ └─────────────────────┘ └┘
typ └─────┘ └──┘ └─────────────────────┘ └┘
doc └─────┘ └──┘
275
276 @[simp] theorem fintype.univ_unit : @univ unit _ = {()} := rfl
id └──┘ └──┘ ┴ ┴└┘ └─┘
src └──┘ └──┘ ┴ ┴└┘ └─┘
typ └──┘ └──┘ ┴ ┴└┘ └─┘
doc └──┘ └──┘ └──┘
277
278 @[simp] theorem fintype.card_unit : fintype.card unit = 1 := rfl
id └──────────┘ └──┘ ┴ └─┘
src └──────────┘ └──┘ ┴ └─┘
typ └──────────┘ └──┘ ┴ └─┘
doc └──┘ └──────────┘ └──┘
279
280 instance : fintype punit := fintype.of_subsingleton punit.star
id └─────┘ └───┘ └─────────────────────┘ └────────┘
src └─────┘ └───┘ └─────────────────────┘ └────────┘
typ └─────┘ └───┘ └─────────────────────┘ └────────┘
doc └─────┘
281
282 @[simp] theorem fintype.univ_punit : @univ punit _ = {punit.star} := rfl
id └──┘ └───┘ ┴ ┴└────────┘ └─┘
src └──┘ └───┘ ┴ ┴└────────┘ └─┘
typ └──┘ └───┘ ┴ ┴└────────┘ └─┘
doc └──┘ └──┘
283
284 @[simp] theorem fintype.card_punit : fintype.card punit = 1 := rfl
id └──────────┘ └───┘ ┴ └─┘
src └──────────┘ └───┘ ┴ └─┘
typ └──────────┘ └───┘ ┴ └─┘
doc └──┘ └──────────┘
285
286 instance : fintype bool := ⟨⟨tt::ff::0, by simp⟩, λ x, by cases x; simp⟩
id └─────┘ └──┘ └┘└┘└┘└┘ ┴ ┴
src └─────┘ └──┘ └┘└┘└┘└┘ └──┘ └────┘ └──┘
typ └─────┘ └──┘ └┘└┘└┘└┘ └──┘ ┴ └────┘┴ └──┘
doc └─────┘ └┘ └┘ └──┘ └────┘ └──┘
txt └──┘ └────┘ └──┘
par └──┘ └────┘ └──┘
pid ┴
st └───┘ └────────────┘
287
288 @[simp] theorem fintype.univ_bool : @univ bool _ = {ff, tt} := rfl
id └──┘ └──┘ ┴ ┴└┘┴ └┘ └─┘
src └──┘ └──┘ ┴ ┴└┘┴ └┘ └─┘
typ └──┘ └──┘ ┴ ┴└┘┴ └┘ └─┘
doc └──┘ └──┘
289
290 instance units_int.fintype : fintype (units ℤ) :=
id └─────┘ └───┘ ┴
src └─────┘ └───┘ ┴
typ └─────┘ └───┘ ┴
doc └─────┘
291 ⟨{1, -1}, λ x, by cases int.units_eq_one_or x; simp *⟩
id ┴ ┴ ┴ ┴ └─────────────────┘ ┴
src ┴ ┴ ┴ └────┘└─────────────────┘┴ └────┘
typ ┴ ┴ ┴ ┴ └────┘└─────────────────┘┴┴ └────┘
doc └────┘ ┴ └────┘
txt └────┘ ┴ └────┘
par └────┘ ┴ └────┘
pid ┴ ┴ ┴┴
st └──────────────────────────────────┘
292
293 instance additive.fintype : Π [fintype α], fintype (additive α) := id
id └─────┘ ┴ └─────┘ └──────┘ ┴ └┘
src └─────┘ └─────┘ └──────┘ └┘
typ └─────┘ ┴ └─────┘ └──────┘ ┴ └┘
doc └─────┘ └─────┘
294
295 instance multiplicative.fintype : Π [fintype α], fintype (multiplicative α) := id
id └─────┘ ┴ └─────┘ └────────────┘ ┴ └┘
src └─────┘ └─────┘ └────────────┘ └┘
typ └─────┘ ┴ └─────┘ └────────────┘ ┴ └┘
doc └─────┘ └─────┘
296
297 @[simp] theorem fintype.card_units_int : fintype.card (units ℤ) = 2 := rfl
id └──────────┘ └───┘ ┴ ┴ └─┘
src └──────────┘ └───┘ ┴ ┴ └─┘
typ └──────────┘ └───┘ ┴ ┴ └─┘
doc └──┘ └──────────┘
298
299 @[simp] theorem fintype.card_bool : fintype.card bool = 2 := rfl
id └──────────┘ └──┘ ┴ └─┘
src └──────────┘ └──┘ ┴ └─┘
typ └──────────┘ └──┘ ┴ └─┘
doc └──┘ └──────────┘
300
301 def finset.insert_none (s : finset α) : finset (option α) :=
id └────┘ ┴ └────┘ └────┘ ┴
src └────┘ └────┘ └────┘
typ └────┘ ┴ └────┘ └────┘ ┴
doc └────┘ └────┘
302 ⟨none :: s.1.map some, multiset.nodup_cons.2
id └──┘ └┘ ┴┴ └─┘ └──┘ └─────────────────┘┴
src └──┘ └┘ ┴ └─┘ └──┘ └─────────────────┘┴
typ └──┘ └┘ ┴┴ └─┘ └──┘ └─────────────────┘┴
doc └┘ └─┘
303 ⟨by simp, multiset.nodup_map (λ a b, option.some.inj) s.2⟩⟩
id └────────────────┘ ┴ ┴ └─────────────┘ ┴┴
src └──┘ └────────────────┘ └─────────────┘ ┴
typ └──┘ └────────────────┘ ┴ ┴ └─────────────┘ ┴┴
doc └──┘
txt └──┘
par └──┘
st └───┘
304
305 @[simp] theorem finset.mem_insert_none {s : finset α} : ∀ {o : option α},
id └────┘ ┴ ┴ └────┘ ┴
src └────┘ └────┘
typ └────┘ ┴ ┴ └────┘ ┴
doc └──┘ └────┘
306 o ∈ s.insert_none ↔ ∀ a ∈ o, a ∈ s
id ┴ ┴ ┴└──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──────────┘ ┴ ┴
typ ┴ ┴ ┴└──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
307 | none := iff_of_true (multiset.mem_cons_self _ _) (λ a h, by cases h)
id └──┘ └─────────┘ └────────────────────┘ ┴ ┴ ┴
src └──┘ └─────────┘ └────────────────────┘ └────┘
typ └──┘ └─────────┘ └────────────────────┘ ┴ ┴ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st └──────┘
308 | (some a) := multiset.mem_cons.trans $ by simp; refl
id └──┘ └───────────────┘└────┘
src └──┘ └───────────────┘└────┘ └──┘ └────
typ └──┘ └───────────────┘└────┘ └──┘ └────
doc └──┘ └────
txt └──┘ └────
par └──┘ └────
pid └
st └───────────
309
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
310 theorem finset.some_mem_insert_none {s : finset α} {a : α} :
id └────┘ ┴ ┴
src └────┘
typ └────┘ ┴ ┴
doc └────┘
311 some a ∈ s.insert_none ↔ a ∈ s := by simp
id └──┘ ┴ ┴ ┴└──────────┘ ┴ ┴ ┴ ┴
src └──┘ ┴ └──────────┘ ┴ ┴ └────
typ └──┘ ┴ ┴ ┴└──────────┘ ┴ ┴ ┴ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
312
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
313 instance {α : Type*} [fintype α] : fintype (option α) :=
id └─────┘ ┴ └─────┘ └────┘ ┴
src └─────┘ └─────┘ └────┘
typ └─────┘ ┴ └─────┘ └────┘ ┴
doc └─────┘ └─────┘
314 ⟨univ.insert_none, λ a, by simp⟩
id └──┘└──────────┘ ┴
src └──┘└──────────┘ └──┘
typ └──┘└──────────┘ ┴ └──┘
doc └──┘ └──┘
txt └──┘
par └──┘
st └───┘
315
316 @[simp] theorem fintype.card_option {α : Type*} [fintype α] :
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
doc └──┘ └─────┘
317 fintype.card (option α) = fintype.card α + 1 :=
id └──────────┘ └────┘ ┴ ┴ └──────────┘ ┴ ┴
src └──────────┘ └────┘ ┴ └──────────┘ ┴
typ └──────────┘ └────┘ ┴ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
318 (multiset.card_cons _ _).trans (by rw multiset.card_map; refl)
id └────────────────┘ └───┘ └───────────────┘
src └────────────────┘ └───┘ └─┘└───────────────┘ └──┘
typ └────────────────┘ └───┘ └─┘└───────────────┘ └──┘
doc └─┘ └──┘
txt └─┘ └──┘
par └─┘ └──┘
pid ┴
st └─────────────────────────┘
319
320 instance {α : Type*} (β : α → Type*)
id ┴
typ ┴
321 [fintype α] [∀ a, fintype (β a)] : fintype (sigma β) :=
id └─────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ └───┘ ┴
src └─────┘ └─────┘ └─────┘ └───┘
typ └─────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ └───┘ ┴
doc └─────┘ └─────┘ └─────┘
322 ⟨univ.sigma (λ _, univ), λ ⟨a, b⟩, by simp⟩
id └──┘└────┘ ┴ └──┘ ┴
src └──┘└────┘ └──┘ └──┘
typ └──┘└────┘ ┴ └──┘ ┴ └──┘
doc └──┘└────┘ └──┘ └──┘
txt └──┘
par └──┘
st └───┘
323
324 @[simp] theorem fintype.card_sigma {α : Type*} (β : α → Type*)
id ┴
typ ┴
doc └──┘
325 [fintype α] [∀ a, fintype (β a)] :
id └─────┘ ┴ ┴ └─────┘ ┴ ┴
src └─────┘ └─────┘
typ └─────┘ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘ └─────┘
326 fintype.card (sigma β) = univ.sum (λ a, fintype.card (β a)) :=
id └──────────┘ └───┘ ┴ ┴ └──┘└──┘ ┴ └──────────┘ ┴ ┴
src └──────────┘ └───┘ ┴ └──┘└──┘ └──────────┘
typ └──────────┘ └───┘ ┴ ┴ └──┘└──┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──┘ └──────────┘
327 card_sigma _ _
id └────────┘
src └────────┘
typ └────────┘
328
329 instance (α β : Type*) [fintype α] [fintype β] : fintype (α × β) :=
id └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
src └─────┘ └─────┘ └─────┘ ┴
typ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └─────┘ └─────┘
330 ⟨univ.product univ, λ ⟨a, b⟩, by simp⟩
id └──┘└──────┘ └──┘ ┴
src └──┘└──────┘ └──┘ └──┘
typ └──┘└──────┘ └──┘ ┴ └──┘
doc └──┘└──────┘ └──┘ └──┘
txt └──┘
par └──┘
st └───┘
331
332 @[simp] theorem fintype.card_prod (α β : Type*) [fintype α] [fintype β] :
id └─────┘ ┴ └─────┘ ┴
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴
doc └──┘ └─────┘ └─────┘
333 fintype.card (α × β) = fintype.card α * fintype.card β :=
id └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴
src └──────────┘ ┴ ┴ └──────────┘ ┴ └──────────┘
typ └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘ └──────────┘
334 card_product _ _
id └──────────┘
src └──────────┘
typ └──────────┘
335
336 def fintype.fintype_prod_left {α β} [decidable_eq α] [fintype (α × β)] [nonempty β] : fintype α :=
id └──────────┘ ┴ └─────┘ ┴ ┴ ┴ └──────┘ ┴ └─────┘ ┴
src └──────────┘ └─────┘ ┴ └──────┘ └─────┘
typ └──────────┘ ┴ └─────┘ ┴ ┴ ┴ └──────┘ ┴ └─────┘ ┴
doc └─────┘ └─────┘
337 ⟨(fintype.elems (α × β)).image prod.fst,
id └───────────┘ ┴ ┴ ┴ └───┘ └──────┘
src └───────────┘ ┴ └───┘ └──────┘
typ └───────────┘ ┴ ┴ ┴ └───┘ └──────┘
doc └───┘
338 assume a, let ⟨b⟩ := ‹nonempty β› in by simp; exact ⟨b, fintype.complete _⟩⟩
id ┴ └─┘ ┴└──────┘ ┴┴ ┴ └──────────────┘
src ┴└──────┘ ┴ └──┘ └────┘ └┘└──────────────┘└─┘
typ ┴ └─┘ ┴└──────┘ ┴┴ └──┘ └────┘ ┴└┘└──────────────┘└─┘
doc ┴ ┴ └──┘ └────┘ └┘ └─┘
txt └──┘ └────┘ └┘ └─┘
par └──┘ └────┘ └┘ └─┘
pid ┴ └┘ └─┘
st └──────────────────────────────────┘
339
340 def fintype.fintype_prod_right {α β} [decidable_eq β] [fintype (α × β)] [nonempty α] : fintype β :=
id └──────────┘ ┴ └─────┘ ┴ ┴ ┴ └──────┘ ┴ └─────┘ ┴
src └──────────┘ └─────┘ ┴ └──────┘ └─────┘
typ └──────────┘ ┴ └─────┘ ┴ ┴ ┴ └──────┘ ┴ └─────┘ ┴
doc └─────┘ └─────┘
341 ⟨(fintype.elems (α × β)).image prod.snd,
id └───────────┘ ┴ ┴ ┴ └───┘ └──────┘
src └───────────┘ ┴ └───┘ └──────┘
typ └───────────┘ ┴ ┴ ┴ └───┘ └──────┘
doc └───┘
342 assume b, let ⟨a⟩ := ‹nonempty α› in by simp; exact ⟨a, fintype.complete _⟩⟩
id ┴ └─┘ ┴└──────┘ ┴┴ ┴ └──────────────┘
src ┴└──────┘ ┴ └──┘ └────┘ └┘└──────────────┘└─┘
typ ┴ └─┘ ┴└──────┘ ┴┴ └──┘ └────┘ ┴└┘└──────────────┘└─┘
doc ┴ ┴ └──┘ └────┘ └┘ └─┘
txt └──┘ └────┘ └┘ └─┘
par └──┘ └────┘ └┘ └─┘
pid ┴ └┘ └─┘
st └──────────────────────────────────┘
343
344 instance (α : Type*) [fintype α] : fintype (ulift α) :=
id └─────┘ ┴ └─────┘ └───┘ ┴
src └─────┘ └─────┘ └───┘
typ └─────┘ ┴ └─────┘ └───┘ ┴
doc └─────┘ └─────┘ └───┘
345 fintype.of_equiv _ equiv.ulift.symm
id └──────────────┘ └─────────┘└───┘
src └──────────────┘ └─────────┘└───┘
typ └──────────────┘ └─────────┘└───┘
doc └──────────────┘
346
347 @[simp] theorem fintype.card_ulift (α : Type*) [fintype α] :
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
doc └──┘ └─────┘
348 fintype.card (ulift α) = fintype.card α :=
id └──────────┘ └───┘ ┴ ┴ └──────────┘ ┴
src └──────────┘ └───┘ ┴ └──────────┘
typ └──────────┘ └───┘ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └───┘ └──────────┘
349 fintype.of_equiv_card _
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
350
351 instance (α : Type u) (β : Type v) [fintype α] [fintype β] : fintype (α ⊕ β) :=
id └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
src └─────┘ └─────┘ └─────┘ ┴
typ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └─────┘ └─────┘
352 @fintype.of_equiv _ _ (@sigma.fintype _
id └──────────────┘ └───────────┘
src └──────────────┘ └───────────┘
typ └──────────────┘ └───────────┘
doc └──────────────┘
353 (λ b, cond b (ulift α) (ulift.{(max u v) v} β)) _
id ┴ └──┘ ┴ └───┘ ┴ └───┘ ┴
src └──┘ └───┘ └───┘
typ ┴ └──┘ ┴ └───┘ ┴ └───┘ ┴
doc └───┘ └───┘
354 (λ b, by cases b; apply ulift.fintype))
id ┴ ┴ └───────────┘
src └────┘ └────┘└───────────┘
typ ┴ └────┘┴ └────┘└───────────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ ┴
st └───────────────────────────┘
355 ((equiv.sum_equiv_sigma_bool _ _).symm.trans
id └────────────────────────┘ └──┘ └───┘
src └────────────────────────┘ └──┘ └───┘
typ └────────────────────────┘ └──┘ └───┘
356 (equiv.sum_congr equiv.ulift equiv.ulift))
id └─────────────┘ └─────────┘ └─────────┘
src └─────────────┘ └─────────┘ └─────────┘
typ └─────────────┘ └─────────┘ └─────────┘
357
358 @[simp] theorem fintype.card_sum (α β : Type*) [fintype α] [fintype β] :
id └─────┘ ┴ └─────┘ ┴
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴
doc └──┘ └─────┘ └─────┘
359 fintype.card (α ⊕ β) = fintype.card α + fintype.card β :=
id └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴
src └──────────┘ ┴ ┴ └──────────┘ ┴ └──────────┘
typ └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘ └──────────┘
360 by rw [sum.fintype, fintype.of_equiv_card]; simp
id └─────────┘ └───────────────────┘
src └──┘└─────────┘└┘└───────────────────┘┴ └────
typ └──┘└─────────┘└┘└───────────────────┘┴ └────
doc └──┘ └┘ ┴ └────
txt └──┘ └┘ ┴ └────
par └──┘ └┘ ┴ └────
pid └┘ └┘ ┴ └
st └──────────────┘└─────────────────────┘┴└──────
361
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
362 lemma fintype.card_le_of_injective [fintype α] [fintype β] (f : α → β)
id └─────┘ ┴ └─────┘ ┴ ┴ ┴
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └─────┘
363 (hf : function.injective f) : fintype.card α ≤ fintype.card β :=
id └────────────────┘ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴
src └────────────────┘ └──────────┘ ┴ └──────────┘
typ └────────────────┘ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘
364 by haveI := classical.prop_decidable; exact
id └──────────────────────┘
src └───────┘└──────────────────────┘ └────┘
typ └───────┘└──────────────────────┘ └────┘
doc └───────┘ └────┘
txt └───────┘ └────┘
par └───────┘ └────┘
pid ┴└─┘ ┴
st └─────────────────────────────────────────
365 finset.card_le_card_of_inj_on f (λ _ _, finset.mem_univ _) (λ _ _ _ _ h, hf h)
id └───────────────────────────┘ ┴ └─────────────┘ └┘
src └───────────────────────────┘┴ ┴ └────┘└─────────────┘└──┘ └──────────┘ ┴ └─
typ └───────────────────────────┘┴┴┴ └────┘└─────────────┘└──┘ └──────────┘└┘┴ └─
doc ┴ ┴ └────┘ └──┘ └──────────┘ ┴ └─
txt ┴ ┴ └────┘ └──┘ └──────────┘ ┴ └─
par ┴ ┴ └────┘ └──┘ └──────────┘ ┴ └─
pid ┴ ┴ └────┘ └──┘ └──────────┘ ┴ ┴└
st ───────────────────────────────────────────────────────────────────────────────
366
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
367 lemma fintype.card_eq_one_iff [fintype α] : fintype.card α = 1 ↔ (∃ x : α, ∀ y, y = x) :=
id └─────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └─────┘ └──────────┘ ┴ ┴ ┴ ┴ ┴
typ └─────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └─────┘ └──────────┘
368 by rw [← fintype.card_unit, fintype.card_eq]; exact
id └───────────────┘ └─────────────┘
src └────┘└───────────────┘└┘└─────────────┘┴ └────┘
typ └────┘└───────────────┘└┘└─────────────┘┴ └────┘
doc └────┘ └┘ ┴ └────┘
txt └────┘ └┘ ┴ └────┘
par └────┘ └┘ ┴ └────┘
pid └──┘ └┘ ┴ ┴
st └──────────────────────┘└───────────────┘┴└───────
369 ⟨λ ⟨a⟩, ⟨a.symm (), λ y, a.injective (subsingleton.elim _ _)⟩,
id ┴ └───┘ └┘ └────────┘
src └┘ └─┘ └───┘┴└┘└┘ └──┘ └────────┘┴ └───────
typ └┘┴└─┘ └───┘┴└┘└┘ └──┘ └────────┘┴ └───────
doc └┘ └─┘ ┴ └┘ └──┘ ┴ └───────
txt └┘ └─┘ ┴ └┘ └──┘ ┴ └───────
par └┘ └─┘ ┴ └┘ └──┘ ┴ └───────
pid └┘ └─┘ ┴ └┘ └──┘ ┴ └───────
st ───────────────────────────────────────────────────────────────
370 λ ⟨x, hx⟩, ⟨⟨λ _, (), λ _, x, λ _, (hx _).trans (hx _).symm,
id ┴ └┘
src ─┘ └┘ └┘ └─┘ └──┘ └┘ └──┘ └┘ └──┘ └────────┘ └─────────
typ ─┘ └┘┴└┘└┘└─┘ └──┘ └┘ └──┘ └┘ └──┘ └────────┘ └─────────
doc ─┘ └┘ └┘ └─┘ └──┘ └┘ └──┘ └┘ └──┘ └────────┘ └─────────
txt ─┘ └┘ └┘ └─┘ └──┘ └┘ └──┘ └┘ └──┘ └────────┘ └─────────
par ─┘ └┘ └┘ └─┘ └──┘ └┘ └──┘ └┘ └──┘ └────────┘ └─────────
pid ─┘ └┘ └┘ └─┘ └──┘ └┘ └──┘ └┘ └──┘ └────────┘ └─────────
st ───────────────────────────────────────────────────────────────
371 λ _, subsingleton.elim _ _⟩⟩⟩
id └───────────────┘
src ───┘ └──┘└───────────────┘└───────
typ ───┘ └──┘└───────────────┘└───────
doc ───┘ └──┘ └───────
txt ───┘ └──┘ └───────
par ───┘ └──┘ └───────
pid ───┘ └──┘ └─────┘└
st ──────────────────────────────────
372
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
373 lemma fintype.card_eq_zero_iff [fintype α] : fintype.card α = 0 ↔ (α → false) :=
id └─────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ └───┘
src └─────┘ └──────────┘ ┴ ┴ └───┘
typ └─────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ └───┘
doc └─────┘ └──────────┘
374 ⟨λ h a, have e : α ≃ empty := classical.choice (fintype.card_eq.1 (by simp [h])), (e a).elim,
id ┴ ┴ ┴ ┴ └───┘ └──────────────┘ └─────────────┘┴ ┴ ┴ ┴ └──┘
src ┴ └───┘ └──────────────┘ └─────────────┘┴ └────┘ ┴ └──┘
typ ┴ ┴ ┴ ┴ └───┘ └──────────────┘ └─────────────┘┴ └────┘┴┴ ┴ ┴ └──┘
doc ┴ └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────┘
375 λ h, have e : α ≃ empty := ⟨λ a, (h a).elim, λ a, a.elim, λ a, (h a).elim, λ a, a.elim⟩,
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └──┘ ┴ ┴└───┘ ┴ ┴ ┴ └──┘ ┴ ┴└───┘
src ┴ └───┘ └──┘ └───┘ └──┘ └───┘
typ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └──┘ ┴ ┴└───┘ ┴ ┴ ┴ └──┘ ┴ ┴└───┘
doc ┴
376 by simp [fintype.card_congr e]⟩
id └────────────────┘ ┴
src └────┘└────────────────┘┴ ┴
typ └────┘└────────────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴┴ ┴ ┴
st └──────────────────────────┘
377
378 lemma fintype.card_pos_iff [fintype α] : 0 < fintype.card α ↔ nonempty α :=
id └─────┘ ┴ ┴ └──────────┘ ┴ ┴ └──────┘ ┴
src └─────┘ ┴ └──────────┘ ┴ └──────┘
typ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ └──────┘ ┴
doc └─────┘ └──────────┘
379 ⟨λ h, classical.by_contradiction (λ h₁,
id ┴ └────────────────────────┘ └┘
src └────────────────────────┘
typ ┴ └────────────────────────┘ └┘
380 have fintype.card α = 0 := fintype.card_eq_zero_iff.2 (λ a, h₁ ⟨a⟩),
id └──────────┘ ┴ ┴ └──────────────────────┘┴ ┴ └┘ ┴
src └──────────┘ ┴ └──────────────────────┘┴
typ └──────────┘ ┴ ┴ └──────────────────────┘┴ ┴ └┘ ┴
doc └──────────┘
381 lt_irrefl 0 $ by rwa this at h),
id └───────┘ └──┘
src └───────┘ └──┘ └───┘
typ └───────┘ └──┘└──┘└───┘
doc └──┘ └───┘
txt └──┘ └───┘
par └──┘ └───┘
pid ┴ └───┘
st └────────────┘
382 λ ⟨a⟩, nat.pos_of_ne_zero (mt fintype.card_eq_zero_iff.1 (λ h, h a))⟩
id ┴┴ └────────────────┘ └┘ └──────────────────────┘┴ ┴ ┴
src └────────────────┘ └┘ └──────────────────────┘┴
typ ┴┴ └────────────────┘ └┘ └──────────────────────┘┴ ┴ ┴
383
384 lemma fintype.card_le_one_iff [fintype α] : fintype.card α ≤ 1 ↔ (∀ a b : α, a = b) :=
id └─────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──────────┘ ┴ ┴ ┴
typ └─────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └──────────┘
385 let n := fintype.card α in
id ┴ └──────────┘ ┴
src └──────────┘
typ ┴ └──────────┘ ┴
doc └──────────┘
386 have hn : n = fintype.card α := rfl,
id ┴ ┴ └──────────┘ ┴ └─┘
src ┴ └──────────┘ └─┘
typ ┴ ┴ └──────────┘ ┴ └─┘
doc └──────────┘
387 match n, hn with
id ┴ └┘
typ ┴ └┘
388 | 0 := λ ha, ⟨λ h, λ a, (fintype.card_eq_zero_iff.1 ha.symm a).elim, λ _, ha ▸ nat.le_succ _⟩
id └┘ ┴ ┴ └──────────────────────┘┴ └┘└───┘ ┴ └──┘ ┴ └┘ ┴ └─────────┘
src └──────────────────────┘┴ └───┘ └──┘ ┴ └─────────┘
typ └┘ ┴ ┴ └──────────────────────┘┴ └┘└───┘ ┴ └──┘ ┴ └┘ ┴ └─────────┘
389 | 1 := λ ha, ⟨λ h, λ a b, let ⟨x, hx⟩ := fintype.card_eq_one_iff.1 ha.symm in
id └┘ ┴ ┴ ┴ └─┘ └─────────────────────┘┴ └┘└───┘
src └─────────────────────┘┴ └───┘
typ └┘ ┴ ┴ ┴ └─┘ └─────────────────────┘┴ └┘└───┘
390 by rw [hx a, hx b],
id └┘ ┴ └┘ ┴
src └──┘ ┴ └┘ ┴ ┴
typ └──┘└┘┴┴└┘└┘┴┴┴
doc └──┘ ┴ └┘ ┴ ┴
txt └──┘ ┴ └┘ ┴ ┴
par └──┘ ┴ └┘ ┴ ┴
pid └┘ ┴ └┘ ┴ ┴
st └───────┘└────┘┴
391 λ _, ha ▸ le_refl _⟩
id ┴ └┘ ┴ └─────┘
src ┴ └─────┘
typ ┴ └┘ ┴ └─────┘
392 | (n+2) := λ ha, ⟨λ h, by rw ← ha at h; exact absurd h dec_trivial,
id ┴ └┘ ┴ └┘ └────┘ ┴ └─────────┘
src ┴ └───┘ └───┘ └────┘└────┘┴ ┴└─────────┘
typ ┴ └┘ ┴ └───┘└┘└───┘ └────┘└────┘┴┴┴└─────────┘
doc └───┘ └───┘ └────┘ ┴ ┴└─────────┘
txt └───┘ └───┘ └────┘ ┴ ┴
par └───┘ └───┘ └────┘ ┴ ┴
pid └─┘ └───┘ ┴ ┴ ┴
st └───────────────────────────────────────┘
393 (λ h, fintype.card_unit ▸ fintype.card_le_of_injective (λ _, ())
id ┴ └───────────────┘ ┴ └──────────────────────────┘ ┴ └┘
src └───────────────┘ ┴ └──────────────────────────┘ └┘
typ ┴ └───────────────┘ ┴ └──────────────────────────┘ ┴ └┘
394 (λ _ _ _, h _ _))⟩
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
395 end
396
397 lemma fintype.exists_ne_of_one_lt_card [fintype α] (h : 1 < fintype.card α) (a : α) :
id └─────┘ ┴ ┴ └──────────┘ ┴ ┴
src └─────┘ ┴ └──────────┘
typ └─────┘ ┴ ┴ └──────────┘ ┴ ┴
doc └─────┘ └──────────┘
398 ∃ b : α, b ≠ a :=
id ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴
399 let ⟨b, hb⟩ := classical.not_forall.1 (mt fintype.card_le_one_iff.2 (not_le_of_gt h)) in
id └─┘ └┘ └──────────────────┘┴ └┘ └─────────────────────┘┴ └──────────┘ ┴
src └──────────────────┘┴ └┘ └─────────────────────┘┴ └──────────┘
typ └─┘ └┘ └──────────────────┘┴ └┘ └─────────────────────┘┴ └──────────┘ ┴
400 let ⟨c, hc⟩ := classical.not_forall.1 hb in
id └─┘ └──────────────────┘┴
src └──────────────────┘┴
typ └─┘ └──────────────────┘┴
401 by haveI := classical.dec_eq α; exact
id └──────────────┘ ┴
src └───────┘└──────────────┘┴ └────┘
typ └───────┘└──────────────┘┴┴ └────┘
doc └───────┘ ┴ └────┘
txt └───────┘ ┴ └────┘
par └───────┘ ┴ └────┘
pid ┴└─┘ ┴ ┴
st └───────────────────────────────────
402 if hba : b = a then ⟨c, by cc⟩ else ⟨b, hba⟩
id └┘ ┴ ┴ ┴ ┴┴
src └┘└─────┘ ┴┴┴ └────┘ └┘ ┴└┘└─────┘ └┘ └─
typ └┘└─────┘ ┴┴┴┴└────┘ ┴└┘ ┴└┘└─────┘┴┴└┘ └─
doc └─────┘ ┴ ┴ └────┘ └┘ ┴└┘└─────┘ └┘ └─
txt └─────┘ ┴ ┴ └────┘ └┘ ┴└┘└─────┘ └┘ └─
par └─────┘ ┴ ┴ └────┘ └┘ ┴└┘└─────┘ └┘ └─
pid └─────┘ ┴ ┴ └────┘ └┘ └────────┘ └┘ ┴└
st ─────────────────────────┘└─┘└───────────────
403
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
404 lemma fintype.injective_iff_surjective [fintype α] {f : α → α} : injective f ↔ surjective f :=
id └─────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └────────┘ ┴
src └─────┘ └───────┘ ┴ └────────┘
typ └─────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └────────┘ ┴
doc └─────┘
405 by haveI := classical.prop_decidable; exact
id └──────────────────────┘
src └───────┘└──────────────────────┘ └────┘
typ └───────┘└──────────────────────┘ └────┘
doc └───────┘ └────┘
txt └───────┘ └────┘
par └───────┘ └────┘
pid ┴└─┘ ┴
st └─────────────────────────────────────────
406 have ∀ {f : α → α}, injective f → surjective f,
id ┴ ┴ └───────┘ └────────┘
src ┴ └────┘ ┴ ┴ ┴ ┴└───────┘┴ ┴ ┴└────────┘┴ └─
typ ┴ └────┘ ┴┴┴┴┴ ┴└───────┘┴ ┴ ┴└────────┘┴ └─
doc ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
txt ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
par ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
st ────────────────────────────────────────────────
407 from λ f hinj x,
src ────┘ └──────────
typ ────┘ └──────────
doc ────┘ └──────────
txt ────┘ └──────────
par ────┘ └──────────
pid ────┘ └──────────
st ─────────────────
408 have h₁ : image f univ = univ := eq_of_subset_of_card_le (subset_univ _)
id ┴ └─────────────────────┘ └─────────┘
src ─┘ └────┘ ┴ ┴ ┴┴┴ └──┘└─────────────────────┘┴ └─────────┘└───
typ ─┘ └────┘ ┴ ┴ ┴┴┴ └──┘└─────────────────────┘┴ └─────────┘└───
doc ─┘ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └───
txt ─┘ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └───
par ─┘ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └───
pid ─┘ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └───
st ───────────────────────────────────────────────────────────────────────────
409 ((card_image_of_injective univ hinj).symm ▸ le_refl _),
id └─────────────────────┘ └──┘ └─────┘
src ───┘ └─────────────────────┘┴└──┘┴ └─────┘ ┴└─────┘└────
typ ───┘ └─────────────────────┘┴└──┘┴ └─────┘ ┴└─────┘└────
doc ───┘ ┴└──┘┴ └─────┘ ┴ └────
txt ───┘ ┴ ┴ └─────┘ ┴ └────
par ───┘ ┴ ┴ └─────┘ ┴ └────
pid ───┘ ┴ ┴ └─────┘ ┴ └────
st ────────────────────────────────────────────────────────────
410 have h₂ : x ∈ image f univ := h₁.symm ▸ mem_univ _,
id ┴ └───┘ └───┘ ┴ └──────┘
src ─┘ └────┘ ┴┴┴└───┘┴ ┴ └──┘ └───┘┴┴┴└──────┘└───
typ ─┘ └────┘ ┴┴┴└───┘┴ ┴ └──┘ └───┘┴┴┴└──────┘└───
doc ─┘ └────┘ ┴ ┴└───┘┴ ┴ └──┘ ┴ ┴ └───
txt ─┘ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └───
par ─┘ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └───
pid ─┘ └────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └───
st ──────────────────────────────────────────────────────
411 exists_of_bex (mem_image.1 h₂),
id └───────────┘ └───────┘
src ─┘└───────────┘┴ └───────┘└─┘ └─┘
typ ─┘└───────────┘┴ └───────┘└─┘ └─┘
doc ─┘ ┴ └─┘ └─┘
txt ─┘ ┴ └─┘ └─┘
par ─┘ ┴ └─┘ └─┘
pid ─┘ ┴ └─┘ └─┘
st ──────────────────────────────────
412 ⟨this,
src └─
typ └─
doc └─
txt └─
par └─
pid └─
st ───────
413 λ hsurj, injective_of_has_left_inverse
id └───────────────────────────┘
src ─┘ └──────┘└───────────────────────────┘└
typ ─┘ └──────┘└───────────────────────────┘└
doc ─┘ └──────┘ └
txt ─┘ └──────┘ └
par ─┘ └──────┘ └
pid ─┘ └──────┘ └
st ─────────────────────────────────────────
414 ⟨surj_inv hsurj, left_inverse_of_surjective_of_right_inverse
id └──────┘ └─────────────────────────────────────────┘
src ───┘ └──────┘┴ └┘└─────────────────────────────────────────┘└
typ ───┘ └──────┘┴ └┘└─────────────────────────────────────────┘└
doc ───┘ └──────┘┴ └┘ └
txt ───┘ ┴ └┘ └
par ───┘ ┴ └┘ └
pid ───┘ ┴ └┘ └
st ─────────────────────────────────────────────────────────────────
415 (this (injective_surj_inv _)) (right_inverse_surj_inv _)⟩⟩
id └────────────────┘ └────────────────────┘
src ─────┘ ┴ └────────────────┘└───┘ └────────────────────┘└─────
typ ─────┘ ┴ └────────────────┘└───┘ └────────────────────┘└─────
doc ─────┘ ┴ └───┘ └─────
txt ─────┘ ┴ └───┘ └─────
par ─────┘ ┴ └───┘ └─────
pid ─────┘ ┴ └───┘ └───┘└
st ─────────────────────────────────────────────────────────────────
416
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
417 lemma fintype.injective_iff_bijective [fintype α] {f : α → α} : injective f ↔ bijective f :=
id └─────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
src └─────┘ └───────┘ ┴ └───────┘
typ └─────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
doc └─────┘
418 by simp [bijective, fintype.injective_iff_surjective]
id └───────┘ └──────────────────────────────┘
src └────┘└───────┘└┘└──────────────────────────────┘└─
typ └────┘└───────┘└┘└──────────────────────────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └───────────────────────────────────────────────────
419
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
420 lemma fintype.surjective_iff_bijective [fintype α] {f : α → α} : surjective f ↔ bijective f :=
id └─────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ └───────┘ ┴
src └─────┘ └────────┘ ┴ └───────┘
typ └─────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ └───────┘ ┴
doc └─────┘
421 by simp [bijective, fintype.injective_iff_surjective]
id └───────┘ └──────────────────────────────┘
src └────┘└───────┘└┘└──────────────────────────────┘└─
typ └────┘└───────┘└┘└──────────────────────────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └───────────────────────────────────────────────────
422
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
423 lemma fintype.injective_iff_surjective_of_equiv [fintype α] {f : α → β} (e : α ≃ β) :
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴
424 injective f ↔ surjective f :=
id └───────┘ ┴ ┴ └────────┘ ┴
src └───────┘ ┴ └────────┘
typ └───────┘ ┴ ┴ └────────┘ ┴
425 have injective (e.symm ∘ f) ↔ surjective (e.symm ∘ f), from fintype.injective_iff_surjective,
id └───────┘ ┴└───┘ ┴ ┴ ┴ └────────┘ ┴└───┘ ┴ ┴ └──────────────────────────────┘
src └───────┘ └───┘ ┴ ┴ └────────┘ └───┘ ┴ └──────────────────────────────┘
typ └───────┘ ┴└───┘ ┴ ┴ ┴ └────────┘ ┴└───┘ ┴ ┴ └──────────────────────────────┘
426 ⟨λ hinj, by simpa [function.comp] using
id └──┘ └───────────┘
src └─────┘└───────────┘└───────
typ └──┘ └─────┘└───────────┘└───────
doc └─────┘ └───────
txt └─────┘ └───────
par └─────┘ └───────
pid ┴┴ ┴┴└─────
st └────────────────────────────
427 surjective_comp e.surjective (this.1 (injective_comp e.symm.injective hinj)),
id └─────────────┘ └──────────┘ └──┘ └────────────┘ └──────────────┘ └──┘
src ─┘└─────────────┘┴└──────────┘┴ └─┘ └────────────┘┴└──────────────┘┴ └┘
typ ─┘└─────────────┘┴└──────────┘┴ └──┘└─┘ └────────────┘┴└──────────────┘┴└──┘└┘
doc ─┘ ┴ ┴ └─┘ ┴ ┴ └┘
txt ─┘ ┴ ┴ └─┘ ┴ ┴ └┘
par ─┘ ┴ ┴ └─┘ ┴ ┴ └┘
pid ─┘ ┴ ┴ └─┘ ┴ ┴ └┘
st ─────────────────────────────────────────────────────────────────────────────┘
428 λ hsurj, by simpa [function.comp] using
id └───┘ └───────────┘
src └─────┘└───────────┘└───────
typ └───┘ └─────┘└───────────┘└───────
doc └─────┘ └───────
txt └─────┘ └───────
par └─────┘ └───────
pid ┴┴ ┴┴└─────
st └────────────────────────────
429 injective_comp e.injective (this.2 (surjective_comp e.symm.surjective hsurj))⟩
id └────────────┘ └─────────┘ └──┘ └─────────────┘ └───────────────┘ └───┘
src ─┘└────────────┘┴└─────────┘┴ └─┘ └─────────────┘┴└───────────────┘┴ └┘
typ ─┘└────────────┘┴└─────────┘┴ └──┘└─┘ └─────────────┘┴└───────────────┘┴└───┘└┘
doc ─┘ ┴ ┴ └─┘ ┴ ┴ └┘
txt ─┘ ┴ ┴ └─┘ ┴ ┴ └┘
par ─┘ ┴ ┴ └─┘ ┴ ┴ └┘
pid ─┘ ┴ ┴ └─┘ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────┘
430
431 instance list.subtype.fintype [decidable_eq α] (l : list α) : fintype {x // x ∈ l} :=
id └──────────┘ ┴ └──┘ ┴ └─────┘ ┴┴ ┴ ┴ ┴
src └──────────┘ └──┘ └─────┘ ┴ ┴
typ └──────────┘ ┴ └──┘ ┴ └─────┘ ┴┴ ┴ ┴ ┴
doc └─────┘
432 fintype.of_list l.attach l.mem_attach
id └─────────────┘ ┴└─────┘ ┴└─────────┘
src └─────────────┘ └─────┘ └─────────┘
typ └─────────────┘ ┴└─────┘ ┴└─────────┘
doc └─────────────┘ └─────┘
433
434 instance multiset.subtype.fintype [decidable_eq α] (s : multiset α) : fintype {x // x ∈ s} :=
id └──────────┘ ┴ └──────┘ ┴ └─────┘ ┴┴ ┴ ┴ ┴
src └──────────┘ └──────┘ └─────┘ ┴ ┴
typ └──────────┘ ┴ └──────┘ ┴ └─────┘ ┴┴ ┴ ┴ ┴
doc └──────┘ └─────┘
435 fintype.of_multiset s.attach s.mem_attach
id └─────────────────┘ ┴└─────┘ ┴└─────────┘
src └─────────────────┘ └─────┘ └─────────┘
typ └─────────────────┘ ┴└─────┘ ┴└─────────┘
doc └─────────────────┘ └─────┘
436
437 instance finset.subtype.fintype (s : finset α) : fintype {x // x ∈ s} :=
id └────┘ ┴ └─────┘ ┴┴ ┴ ┴ ┴
src └────┘ └─────┘ ┴ ┴
typ └────┘ ┴ └─────┘ ┴┴ ┴ ┴ ┴
doc └────┘ └─────┘
438 ⟨s.attach, s.mem_attach⟩
id ┴└─────┘ ┴└─────────┘
src └─────┘ └─────────┘
typ ┴└─────┘ ┴└─────────┘
doc └─────┘
439
440 instance finset_coe.fintype (s : finset α) : fintype (↑s : set α) :=
id └────┘ ┴ └─────┘ ┴┴ └─┘ ┴
src └────┘ └─────┘ ┴ └─┘
typ └────┘ ┴ └─────┘ ┴┴ └─┘ ┴
doc └────┘ └─────┘
441 finset.subtype.fintype s
id └────────────────────┘ ┴
src └────────────────────┘
typ └────────────────────┘ ┴
442
443 @[simp] lemma fintype.card_coe (s : finset α) :
id └────┘ ┴
src └────┘
typ └────┘ ┴
doc └──┘ └────┘
444 fintype.card (↑s : set α) = s.card := card_attach
id └──────────┘ ┴┴ └─┘ ┴ ┴ ┴└───┘ └─────────┘
src └──────────┘ ┴ └─┘ ┴ └───┘ └─────────┘
typ └──────────┘ ┴┴ └─┘ ┴ ┴ ┴└───┘ └─────────┘
doc └──────────┘ └───┘
445
446 instance plift.fintype (p : Prop) [decidable p] : fintype (plift p) :=
id └───────┘ ┴ └─────┘ └───┘ ┴
src └───────┘ └─────┘ └───┘
typ └───────┘ ┴ └─────┘ └───┘ ┴
doc └─────┘ └───┘
447 ⟨if h : p then finset.singleton ⟨h⟩ else ∅, λ ⟨h⟩, by simp [h]⟩
id └┘ ┴ └──────────────┘ ┴ ┴ ┴ ┴
src └┘ └──────────────┘ ┴ └────┘ ┴
typ └┘ ┴ └──────────────┘ ┴ ┴ ┴ └────┘┴┴
doc └──────────────┘ └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────┘
448
449 instance Prop.fintype : fintype Prop :=
id └─────┘
src └─────┘
typ └─────┘
doc └─────┘
450 ⟨⟨true::false::0, by simp [true_ne_false]⟩,
id └──┘└┘└───┘└┘ └───────────┘
src └──┘└┘└───┘└┘ └────┘└───────────┘┴
typ └──┘└┘└───┘└┘ └────┘└───────────┘┴
doc └┘ └┘ └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────────────────┘
451 classical.cases (by simp) (by simp)⟩
id └─────────────┘
src └─────────────┘ └──┘ └──┘
typ └─────────────┘ └──┘ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
st └───┘ └───┘
452
453 def set_fintype {α} [fintype α] (s : set α) [decidable_pred s] : fintype s :=
id └─────┘ ┴ └─┘ ┴ └────────────┘ ┴ └─────┘ ┴
src └─────┘ └─┘ └────────────┘ └─────┘
typ └─────┘ ┴ └─┘ ┴ └────────────┘ ┴ └─────┘ ┴
doc └─────┘ └─────┘
454 fintype.subtype (univ.filter (∈ s)) (by simp)
id └─────────────┘ └──┘└─────┘ ┴ ┴
src └─────────────┘ └──┘└─────┘ ┴ └──┘
typ └─────────────┘ └──┘└─────┘ ┴ ┴ └──┘
doc └──┘└─────┘ └──┘
txt └──┘
par └──┘
st └───┘
455
456 instance pi.fintype {α : Type*} {β : α → Type*}
id ┴
typ ┴
457 [fintype α] [decidable_eq α] [∀a, fintype (β a)] : fintype (Πa, β a) :=
id └─────┘ ┴ └──────────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
src └─────┘ └──────────┘ └─────┘ └─────┘
typ └─────┘ ┴ └──────────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └─────┘ └─────┘
458 @fintype.of_equiv _ _
id └──────────────┘
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
459 ⟨univ.pi $ λa:α, @univ (β a) _,
id └──┘└─┘ ┴ └──┘ ┴ ┴
src └──┘└─┘ └──┘
typ └──┘└─┘ ┴ └──┘ ┴ ┴
doc └──┘ └──┘
460 λ f, finset.mem_pi.2 $ λ a ha, mem_univ _⟩
id ┴ └───────────┘┴ ┴ └┘ └──────┘
src └───────────┘┴ └──────┘
typ ┴ └───────────┘┴ ┴ └┘ └──────┘
461 ⟨λ f a, f a (mem_univ _), λ f a _, f a, λ f, rfl, λ f, rfl⟩
id ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘
src └──────┘ └─┘ └─┘
typ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘
462
463 @[simp] lemma fintype.card_pi {β : α → Type*} [fintype α] [decidable_eq α]
id ┴ └─────┘ ┴ └──────────┘ ┴
src └─────┘ └──────────┘
typ ┴ └─────┘ ┴ └──────────┘ ┴
doc └──┘ └─────┘
464 [f : Π a, fintype (β a)] : fintype.card (Π a, β a) = univ.prod (λ a, fintype.card (β a)) :=
id ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └──┘└───┘ ┴ └──────────┘ ┴ ┴
src └─────┘ └──────────┘ ┴ └──┘└───┘ └──────────┘
typ ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ └──┘└───┘ ┴ └──────────┘ ┴ ┴
doc └─────┘ └──────────┘ └──┘└───┘ └──────────┘
465 by letI f' : fintype (Πa∈univ, β a) :=
id └─────┘ └──┘ ┴
src └────────┘└─────┘┴ └┘└──┘ ┴ ┴ └────
typ └────────┘└─────┘┴ └┘└──┘ ┴┴┴ └────
doc └────────┘└─────┘┴ └┘└──┘ ┴ ┴ └────
txt └────────┘ ┴ └┘ ┴ ┴ └────
par └────────┘ ┴ └┘ ┴ ┴ └────
pid └─┘└─┘ ┴ └┘ ┴ ┴ ┴└───
st └────────────────────────────────────
466 ⟨(univ.pi $ λa, univ), assume f, finset.mem_pi.2 $ assume a ha, mem_univ _⟩;
id └─────┘ └──┘ └───────────┘ └──────┘
src ─┘ └─────┘┴ ┴ └─┘└──┘└─┘ └──┘└───────────┘└─┘ ┴ └─────┘└──────┘└─┘
typ ─┘ └─────┘┴ ┴ └─┘└──┘└─┘ └──┘└───────────┘└─┘ ┴ └─────┘└──────┘└─┘
doc ─┘ ┴ ┴ └─┘└──┘└─┘ └──┘ └─┘ ┴ └─────┘ └─┘
txt ─┘ ┴ ┴ └─┘ └─┘ └──┘ └─┘ ┴ └─────┘ └─┘
par ─┘ ┴ ┴ └─┘ └─┘ └──┘ └─┘ ┴ └─────┘ └─┘
pid ─┘ ┴ ┴ └─┘ └─┘ └──┘ └─┘ ┴ └─────┘ └─┘
st ───────────────────────────────────────────────────────────────────────────────
467 exact calc fintype.card (Π a, β a) = fintype.card (Π a ∈ univ, β a) : fintype.card_congr
id └────────────────┘
src └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ └──┘└────────────────┘└
typ └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ └──┘└────────────────┘└
doc └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ └──┘ └
txt └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ └──┘ └
par └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ └──┘ └
pid ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ └──┘ └
st ─────────────────────────────────────────────────────────────────────────────────────────
468 ⟨λ f a ha, f a, λ f a, f a (mem_univ a), λ _, rfl, λ _, rfl⟩
id └──────┘ └─┘
src ─┘ └───────┘ ┴ └┘ └────┘ ┴ ┴ └──────┘┴ └─┘ └──┘ └┘ └──┘└─┘└─
typ ─┘ └───────┘ ┴ └┘ └────┘ ┴ ┴ └──────┘┴ └─┘ └──┘ └┘ └──┘└─┘└─
doc ─┘ └───────┘ ┴ └┘ └────┘ ┴ ┴ ┴ └─┘ └──┘ └┘ └──┘ └─
txt ─┘ └───────┘ ┴ └┘ └────┘ ┴ ┴ ┴ └─┘ └──┘ └┘ └──┘ └─
par ─┘ └───────┘ ┴ └┘ └────┘ ┴ ┴ ┴ └─┘ └──┘ └┘ └──┘ └─
pid ─┘ └───────┘ ┴ └┘ └────┘ ┴ ┴ ┴ └─┘ └──┘ └┘ └──┘ └─
st ───────────────────────────────────────────────────────────────
469 ... = univ.prod (λ a, fintype.card (β a)) : finset.card_pi _ _
id └───────┘ └──────────┘ ┴ └────────────┘
src ───┘ ┴└───────┘┴ └──┘└──────────┘┴ ┴ └───┘└────────────┘└────
typ ───┘ ┴└───────┘┴ └──┘└──────────┘┴ ┴┴ └───┘└────────────┘└────
doc ───┘ ┴└───────┘┴ └──┘└──────────┘┴ ┴ └───┘ └────
txt ───┘ ┴ ┴ └──┘ ┴ ┴ └───┘ └────
par ───┘ ┴ ┴ └──┘ ┴ ┴ └───┘ └────
pid ───┘ ┴ ┴ └──┘ ┴ ┴ └───┘ └──┘└
st ───────────────────────────────────────────────────────────────
470
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
471 @[simp] lemma fintype.card_fun [fintype α] [decidable_eq α] [fintype β] :
id └─────┘ ┴ └──────────┘ ┴ └─────┘ ┴
src └─────┘ └──────────┘ └─────┘
typ └─────┘ ┴ └──────────┘ ┴ └─────┘ ┴
doc └──┘ └─────┘ └─────┘
472 fintype.card (α → β) = fintype.card β ^ fintype.card α :=
id └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴
src └──────────┘ ┴ └──────────┘ ┴ └──────────┘
typ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘ └──────────┘
473 by rw [fintype.card_pi, finset.prod_const, nat.pow_eq_pow]; refl
id └─────────────┘ └───────────────┘ └────────────┘
src └──┘└─────────────┘└┘└───────────────┘└┘└────────────┘┴ └────
typ └──┘└─────────────┘└┘└───────────────┘└┘└────────────┘┴ └────
doc └──┘ └┘ └┘ ┴ └────
txt └──┘ └┘ └┘ ┴ └────
par └──┘ └┘ └┘ ┴ └────
pid └┘ └┘ └┘ ┴ └
st └──────────────────┘└─────────────────┘└──────────────┘┴└──────
474
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
475 instance d_array.fintype {n : ℕ} {α : fin n → Type*}
id ┴ └─┘ ┴
src ┴ └─┘
typ ┴ └─┘ ┴
476 [∀n, fintype (α n)] : fintype (d_array n α) :=
id ┴ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴
src └─────┘ └─────┘ └─────┘
typ ┴ └─────┘ ┴ ┴ └─────┘ └─────┘ ┴ ┴
doc └─────┘ └─────┘
477 fintype.of_equiv _ (equiv.d_array_equiv_fin _).symm
id └──────────────┘ └─────────────────────┘ └──┘
src └──────────────┘ └─────────────────────┘ └──┘
typ └──────────────┘ └─────────────────────┘ └──┘
doc └──────────────┘
478
479 instance array.fintype {n : ℕ} {α : Type*} [fintype α] : fintype (array n α) :=
id ┴ └─────┘ ┴ └─────┘ └───┘ ┴ ┴
src ┴ └─────┘ └─────┘ └───┘
typ ┴ └─────┘ ┴ └─────┘ └───┘ ┴ ┴
doc └─────┘ └─────┘
480 d_array.fintype
id └─────────────┘
src └─────────────┘
typ └─────────────┘
481
482 instance vector.fintype {α : Type*} [fintype α] {n : ℕ} : fintype (vector α n) :=
id └─────┘ ┴ ┴ └─────┘ └────┘ ┴ ┴
src └─────┘ ┴ └─────┘ └────┘
typ └─────┘ ┴ ┴ └─────┘ └────┘ ┴ ┴
doc └─────┘ └─────┘
483 fintype.of_equiv _ (equiv.vector_equiv_fin _ _).symm
id └──────────────┘ └────────────────────┘ └──┘
src └──────────────┘ └────────────────────┘ └──┘
typ └──────────────┘ └────────────────────┘ └──┘
doc └──────────────┘
484
485 @[simp] lemma card_vector [fintype α] (n : ℕ) :
id └─────┘ ┴ ┴
src └─────┘ ┴
typ └─────┘ ┴ ┴
doc └──┘ └─────┘
486 fintype.card (vector α n) = fintype.card α ^ n :=
id └──────────┘ └────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ └────┘ ┴ └──────────┘ ┴
typ └──────────┘ └────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘
487 by rw fintype.of_equiv_card; simp
id └───────────────────┘
src └─┘└───────────────────┘ └────
typ └─┘└───────────────────┘ └────
doc └─┘ └────
txt └─┘ └────
par └─┘ └────
pid ┴ └
st └───────────────────────────────
488
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
489 instance quotient.fintype [fintype α] (s : setoid α)
id └─────┘ ┴ └────┘ ┴
src └─────┘ └────┘
typ └─────┘ ┴ └────┘ ┴
doc └─────┘
490 [decidable_rel ((≈) : α → α → Prop)] : fintype (quotient s) :=
id └───────────┘ ┴ ┴ ┴ └─────┘ └──────┘ ┴
src └───────────┘ ┴ └─────┘ └──────┘
typ └───────────┘ ┴ ┴ ┴ └─────┘ └──────┘ ┴
doc └─────┘
491 fintype.of_surjective quotient.mk (λ x, quotient.induction_on x (λ x, ⟨x, rfl⟩))
id └───────────────────┘ └─────────┘ ┴ └───────────────────┘ ┴ ┴ ┴ └─┘
src └───────────────────┘ └─────────┘ └───────────────────┘ └─┘
typ └───────────────────┘ └─────────┘ ┴ └───────────────────┘ ┴ ┴ ┴ └─┘
doc └───────────────────┘
492
493 instance finset.fintype [fintype α] : fintype (finset α) :=
id └─────┘ ┴ └─────┘ └────┘ ┴
src └─────┘ └─────┘ └────┘
typ └─────┘ ┴ └─────┘ └────┘ ┴
doc └─────┘ └─────┘ └────┘
494 ⟨univ.powerset, λ x, finset.mem_powerset.2 (finset.subset_univ _)⟩
id └──┘└───────┘ ┴ └─────────────────┘┴ └────────────────┘
src └──┘└───────┘ └─────────────────┘┴ └────────────────┘
typ └──┘└───────┘ ┴ └─────────────────┘┴ └────────────────┘
doc └──┘└───────┘
495
496 instance subtype.fintype [fintype α] (p : α → Prop) [decidable_pred p] : fintype {x // p x} :=
id └─────┘ ┴ ┴ └────────────┘ ┴ └─────┘ ┴┴ ┴ ┴
src └─────┘ └────────────┘ └─────┘ ┴
typ └─────┘ ┴ ┴ └────────────┘ ┴ └─────┘ ┴┴ ┴ ┴
doc └─────┘ └─────┘
497 set_fintype _
id └─────────┘
src └─────────┘
typ └─────────┘
498
499 theorem fintype.card_subtype_le [fintype α] (p : α → Prop) [decidable_pred p] :
id └─────┘ ┴ ┴ └────────────┘ ┴
src └─────┘ └────────────┘
typ └─────┘ ┴ ┴ └────────────┘ ┴
doc └─────┘
500 fintype.card {x // p x} ≤ fintype.card α :=
id └──────────┘ ┴┴ ┴ ┴ ┴ └──────────┘ ┴
src └──────────┘ ┴ ┴ └──────────┘
typ └──────────┘ ┴┴ ┴ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘
501 by rw fintype.subtype_card; exact card_le_of_subset (subset_univ _)
id └──────────────────┘ └───────────────┘ └─────────┘
src └─┘└──────────────────┘ └────┘└───────────────┘┴ └─────────┘└───
typ └─┘└──────────────────┘ └────┘└───────────────┘┴ └─────────┘└───
doc └─┘ └────┘ ┴ └───
txt └─┘ └────┘ ┴ └───
par └─┘ └────┘ ┴ └───
pid ┴ ┴ ┴ └─┘└
st └─────────────────────────────────────────────────────────────────
502
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
503 theorem fintype.card_subtype_lt [fintype α] {p : α → Prop} [decidable_pred p]
id └─────┘ ┴ ┴ └────────────┘ ┴
src └─────┘ └────────────┘
typ └─────┘ ┴ ┴ └────────────┘ ┴
doc └─────┘
504 {x : α} (hx : ¬ p x) : fintype.card {x // p x} < fintype.card α :=
id ┴ ┴ ┴ ┴ └──────────┘ ┴┴ ┴ ┴ ┴ └──────────┘ ┴
src ┴ └──────────┘ ┴ ┴ └──────────┘
typ ┴ ┴ ┴ ┴ └──────────┘ ┴┴ ┴ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘
505 by rw [fintype.subtype_card]; exact finset.card_lt_card
id └──────────────────┘ └─────────────────┘
src └──┘└──────────────────┘┴ └────┘└─────────────────┘└
typ └──┘└──────────────────┘┴ └────┘└─────────────────┘└
doc └──┘ ┴ └────┘ └
txt └──┘ ┴ └────┘ └
par └──┘ ┴ └────┘ └
pid └┘ ┴ ┴ └
st └───────────────────────┘┴└───────────────────────────
506 ⟨subset_univ _, classical.not_forall.2 ⟨x, by simp [*, set.mem_def]⟩⟩
id └─────────┘ └──────────────────┘ ┴ └─────────┘
src ─┘ └─────────┘└──┘└──────────────────┘└─┘ └┘ ┴└───────┘└─────────┘┴└──
typ ─┘ └─────────┘└──┘└──────────────────┘└─┘ ┴└┘ ┴└───────┘└─────────┘┴└──
doc ─┘ └──┘ └─┘ └┘ ┴└───────┘ ┴└──
txt ─┘ └──┘ └─┘ └┘ ┴└───────┘ ┴└──
par ─┘ └──┘ └─┘ └┘ ┴└───────┘ ┴└──
pid ─┘ └──┘ └─┘ └┘ └────────┘ └─┘└
st ──────────────────────────────────────────────┘└────────────────────┘└──
507
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
508 instance psigma.fintype {α : Type*} {β : α → Type*} [fintype α] [∀ a, fintype (β a)] :
id ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴
src └─────┘ └─────┘
typ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘ └─────┘
509 fintype (Σ' a, β a) :=
id └─────┘ └┘ ┴┴ ┴ ┴
src └─────┘ └┘ ┴
typ └─────┘ └┘ ┴┴ ┴ ┴
doc └─────┘
510 fintype.of_equiv _ (equiv.psigma_equiv_sigma _).symm
id └──────────────┘ └──────────────────────┘ └──┘
src └──────────────┘ └──────────────────────┘ └──┘
typ └──────────────┘ └──────────────────────┘ └──┘
doc └──────────────┘
511
512 instance psigma.fintype_prop_left {α : Prop} {β : α → Type*} [∀ a, fintype (β a)] [decidable α] :
id ┴ ┴ └─────┘ ┴ ┴ └───────┘ ┴
src └─────┘ └───────┘
typ ┴ ┴ └─────┘ ┴ ┴ └───────┘ ┴
doc └─────┘
513 fintype (Σ' a, β a) :=
id └─────┘ └┘ ┴┴ ┴ ┴
src └─────┘ └┘ ┴
typ └─────┘ └┘ ┴┴ ┴ ┴
doc └─────┘
514 if h : α then fintype.of_equiv (β h) ⟨λ x, ⟨h, x⟩, psigma.snd, λ _, rfl, λ ⟨_, _⟩, rfl⟩
id └┘ ┴ └──────────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ └─┘ ┴ └─┘
src └┘ └──────────────┘ └────────┘ └─┘ └─┘
typ └┘ ┴ └──────────────┘ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ └─┘ ┴ └─┘
doc └──────────────┘
515 else ⟨∅, λ x, h x.1⟩
id ┴┴ ┴ ┴ ┴┴
src ┴ ┴
typ ┴┴ ┴ ┴ ┴┴
516
517 instance psigma.fintype_prop_right {α : Type*} {β : α → Prop} [fintype α] [∀ a, decidable (β a)] :
id ┴ └─────┘ ┴ ┴ └───────┘ ┴ ┴
src └─────┘ └───────┘
typ ┴ └─────┘ ┴ ┴ └───────┘ ┴ ┴
doc └─────┘
518 fintype (Σ' a, β a) :=
id └─────┘ └┘ ┴┴ ┴ ┴
src └─────┘ └┘ ┴
typ └─────┘ └┘ ┴┴ ┴ ┴
doc └─────┘
519 fintype.of_equiv {a // β a} ⟨λ ⟨x, y⟩, ⟨x, y⟩, λ ⟨x, y⟩, ⟨x, y⟩, λ ⟨x, y⟩, rfl, λ ⟨x, y⟩, rfl⟩
id └──────────────┘ ┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ └─┘
src └──────────────┘ ┴ └─┘ └─┘
typ └──────────────┘ ┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ └─┘
doc └──────────────┘
520
521 instance psigma.fintype_prop_prop {α : Prop} {β : α → Prop} [decidable α] [∀ a, decidable (β a)] :
id ┴ └───────┘ ┴ ┴ └───────┘ ┴ ┴
src └───────┘ └───────┘
typ ┴ └───────┘ ┴ ┴ └───────┘ ┴ ┴
522 fintype (Σ' a, β a) :=
id └─────┘ └┘ ┴┴ ┴ ┴
src └─────┘ └┘ ┴
typ └─────┘ └┘ ┴┴ ┴ ┴
doc └─────┘
523 if h : ∃ a, β a then ⟨{⟨h.fst, h.snd⟩}, λ ⟨_, _⟩, by simp⟩ else ⟨∅, λ ⟨x, y⟩, h ⟨x, y⟩⟩
id └┘ ┴ ┴┴ ┴ ┴ ┴ ┴└──┘ ┴└──┘ ┴ ┴┴ ┴┴ ┴ ┴
src └┘ ┴ ┴ ┴ └──┘ └──┘ └──┘ ┴
typ └┘ ┴ ┴┴ ┴ ┴ ┴ ┴└──┘ ┴└──┘ ┴ └──┘ ┴┴ ┴┴ ┴ ┴
doc └──┘
txt └──┘
par └──┘
st └───┘
524
525 instance set.fintype [fintype α] [decidable_eq α] : fintype (set α) :=
id └─────┘ ┴ └──────────┘ ┴ └─────┘ └─┘ ┴
src └─────┘ └──────────┘ └─────┘ └─┘
typ └─────┘ ┴ └──────────┘ ┴ └─────┘ └─┘ ┴
doc └─────┘ └─────┘
526 pi.fintype
id └────────┘
src └────────┘
typ └────────┘
527
528 instance pfun_fintype (p : Prop) [decidable p] (α : p → Type*)
id └───────┘ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴
529 [Π hp, fintype (α hp)] : fintype (Π hp : p, α hp) :=
id └┘ └─────┘ ┴ └┘ └─────┘ ┴ ┴ └┘
src └─────┘ └─────┘
typ └┘ └─────┘ ┴ └┘ └─────┘ ┴ ┴ └┘
doc └─────┘ └─────┘
530 if hp : p then fintype.of_equiv (α hp) ⟨λ a _, a, λ f, f hp, λ _, rfl, λ _, rfl⟩
id └┘ ┴ └──────────────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └─┘
src └┘ └──────────────┘ └─┘ └─┘
typ └┘ ┴ └──────────────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └─┘
doc └──────────────┘
531 else ⟨singleton (λ h, (hp h).elim), by simp [hp, function.funext_iff]⟩
id ┴└───────┘ ┴ └┘ ┴ └──┘ └┘ └─────────────────┘
src └───────┘ └──┘ └────┘ └┘└─────────────────┘┴
typ ┴└───────┘ ┴ └┘ ┴ └──┘ └────┘└┘└┘└─────────────────┘┴
doc └───────┘ └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └─────────────────────────────┘
532
533 def quotient.fin_choice_aux {ι : Type*} [decidable_eq ι]
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
534 {α : ι → Type*} [S : ∀ i, setoid (α i)] :
id ┴ ┴ └────┘ ┴ ┴
src └────┘
typ ┴ ┴ └────┘ ┴ ┴
535 ∀ (l : list ι), (∀ i ∈ l, quotient (S i)) → @quotient (Π i ∈ l, α i) (by apply_instance)
id ┴ └──┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──┘ └──────┘ └──────┘ └────────────┘
typ ┴ └──┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
st └─────────────┘
536 | [] f := ⟦λ i, false.elim⟧
id └┘ ┴ ┴ └────────┘┴
src └┘ ┴ └────────┘┴
typ └┘ ┴ ┴ └────────┘┴
537 | (i::l) f := begin
id └┘
src └┘
typ └┘
st └─────
538 refine quotient.lift_on₂ (f i (list.mem_cons_self _ _))
id └───────────────┘ ┴ └────────────────┘
src └─────┘└───────────────┘┴ ┴ ┴ └────────────────┘└──────
typ └─────┘└───────────────┘┴ ┴┴┴ └────────────────┘└──────
doc └─────┘ ┴ ┴ ┴ └──────
txt └─────┘ ┴ ┴ ┴ └──────
par └─────┘ ┴ ┴ ┴ └──────
pid ┴ ┴ ┴ ┴ └──────
st ──────────────────────────────────────────────────────────
539 (quotient.fin_choice_aux l (λ j h, f j (list.mem_cons_of_mem _ h)))
id └─────────────────────┘ ┴ ┴ └──────────────────┘
src ───┘ ┴ ┴ └────┘ ┴ ┴ └──────────────────┘└─┘ └───
typ ───┘ └─────────────────────┘┴┴┴ └────┘┴┴ ┴ └──────────────────┘└─┘ └───
doc ───┘ ┴ ┴ └────┘ ┴ ┴ └─┘ └───
txt ───┘ ┴ ┴ └────┘ ┴ ┴ └─┘ └───
par ───┘ ┴ ┴ └────┘ ┴ ┴ └─┘ └───
pid ───┘ ┴ ┴ └────┘ ┴ ┴ └─┘ └───
st ────────────────────────────────────────────────────────────────────────
540 _ _,
src ──────┘
typ ──────┘
doc ──────┘
txt ──────┘
par ──────┘
pid ──────┘
st ──────┘└─
541 exact λ a l, ⟦λ j h,
id ┴
src └────┘ └────┘┴ └─────
typ └────┘ └────┘┴ └─────
doc └────┘ └────┘ └─────
txt └────┘ └────┘ └─────
par └────┘ └────┘ └─────
pid ┴ └────┘ └─────
st ───────────────────────
542 if e : j = i then by rw e; exact a else
id └┘ ┴ ┴ ┴ ┴
src ───┘└┘└───┘ ┴┴┴ └────┘ ┴└─┘ └──────┘ └─────
typ ───┘└┘└───┘ ┴┴┴┴└────┘ ┴└─┘┴└──────┘┴└─────
doc ───┘ └───┘ ┴ ┴ └────┘ ┴└─┘ └──────┘ └─────
txt ───┘ └───┘ ┴ ┴ └────┘ ┴└─┘ └──────┘ └─────
par ───┘ └───┘ ┴ ┴ └────┘ ┴└─┘ └──────┘ └─────
pid ───┘ └───┘ ┴ ┴ └────┘ └──┘ └──────┘ └─────
st ───────────────────────┘└─────────────┘└────
543 l _ (h.resolve_left e)⟧,
id ┴ └───────────┘ ┴
src ───┘ └─┘ └───────────┘┴ ┴┴
typ ───┘┴└─┘ └───────────┘┴ ┴┴
doc ───┘ └─┘ ┴ ┴
txt ───┘ └─┘ ┴ ┴
par ───┘ └─┘ ┴ ┴
pid ───┘ └─┘ ┴ ┴
st ──────────────────────────┘└─
544 refine λ a₁ l₁ a₂ l₂ h₁ h₂, quotient.sound (λ j h, _),
id └────────────┘
src └─────┘ └──────────────────┘└────────────┘┴ └──────┘
typ └─────┘ └──────────────────┘└────────────┘┴ └──────┘
doc └─────┘ └──────────────────┘ ┴ └──────┘
txt └─────┘ └──────────────────┘ ┴ └──────┘
par └─────┘ └──────────────────┘ ┴ └──────┘
pid ┴ └──────────────────┘ ┴ └──────┘
st ──────────────────────────────────────────────────────┘└─
545 by_cases e : j = i; simp [e],
id ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴ └────┘ ┴
typ └───────┘ └─┘┴┴ ┴┴ └────┘┴┴
doc └───────┘ └─┘ ┴ ┴ └────┘ ┴
txt └───────┘ └─┘ ┴ ┴ └────┘ ┴
par └───────┘ └─┘ ┴ ┴ └────┘ ┴
pid ┴ └─┘ ┴ ┴ ┴┴ ┴
st ─────────────────────────────┘└─
546 { subst j, exact h₁ },
id ┴ └┘
src └────┘ └────┘ ┴
typ └────┘┴ └────┘└┘┴
doc └────┘ └────┘ ┴
txt └────┘ └────┘ ┴
par └────┘ └────┘ ┴
pid ┴ ┴ ┴
st ───┘└─────┘└─────────┘└┘└
547 { exact h₂ _ _ }
id └┘
src └────┘ └───┘
typ └────┘└┘└───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ └──┘┴
st ────────────────┘└─
548 end
st ──┘
549
550 theorem quotient.fin_choice_aux_eq {ι : Type*} [decidable_eq ι]
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
551 {α : ι → Type*} [S : ∀ i, setoid (α i)] :
id ┴ ┴ └────┘ ┴ ┴
src └────┘
typ ┴ ┴ └────┘ ┴ ┴
552 ∀ (l : list ι) (f : ∀ i ∈ l, α i), quotient.fin_choice_aux l (λ i h, ⟦f i h⟧) = ⟦f⟧
id ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─────────────────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴
src └──┘ └─────────────────────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─────────────────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴
553 | [] f := quotient.sound (λ i h, h.elim)
id └┘ └────────────┘ ┴ ┴ ┴└───┘
src └┘ └────────────┘ └───┘
typ └┘ └────────────┘ ┴ ┴ ┴└───┘
554 | (i::l) f := begin
id └┘
src └┘
typ └┘
st └─────
555 simp [quotient.fin_choice_aux, quotient.fin_choice_aux_eq l],
id └─────────────────────┘ └────────────────────────┘ ┴
src └────┘└─────────────────────┘└┘ ┴ ┴
typ └────┘└─────────────────────┘└┘└────────────────────────┘┴┴┴
doc └────┘ └┘ ┴ ┴
txt └────┘ └┘ ┴ ┴
par └────┘ └┘ ┴ ┴
pid ┴┴ └┘ ┴ ┴
st ─────────────────────────────────────────────────────────────┘└─
556 refine quotient.sound (λ j h, _),
id └────────────┘
src └─────┘└────────────┘┴ └──────┘
typ └─────┘└────────────┘┴ └──────┘
doc └─────┘ ┴ └──────┘
txt └─────┘ ┴ └──────┘
par └─────┘ ┴ └──────┘
pid ┴ ┴ └──────┘
st ─────────────────────────────────┘└─
557 by_cases e : j = i; simp [e],
id ┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴┴┴ └────┘ ┴
typ └───────┘ └─┘┴┴┴┴┴ └────┘┴┴
doc └───────┘ └─┘ ┴ ┴ └────┘ ┴
txt └───────┘ └─┘ ┴ ┴ └────┘ ┴
par └───────┘ └─┘ ┴ ┴ └────┘ ┴
pid ┴ └─┘ ┴ ┴ ┴┴ ┴
st ─────────────────────────────┘└─
558 subst j, refl
id ┴
src └────┘ └───┘
typ └────┘┴ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st ────────┘└─────┘
559 end
st └─┘
560
561 def quotient.fin_choice {ι : Type*} [fintype ι] [decidable_eq ι]
id └─────┘ ┴ └──────────┘ ┴
src └─────┘ └──────────┘
typ └─────┘ ┴ └──────────┘ ┴
doc └─────┘
562 {α : ι → Type*} [S : ∀ i, setoid (α i)]
id ┴ ┴ └────┘ ┴ ┴
src └────┘
typ ┴ ┴ └────┘ ┴ ┴
563 (f : ∀ i, quotient (S i)) : @quotient (Π i, α i) (by apply_instance) :=
id ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴ ┴
src └──────┘ └──────┘ └────────────┘
typ ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
st └─────────────┘
564 quotient.lift_on (@quotient.rec_on _ _ (λ l : multiset ι,
id └──────────────┘ └─────────────┘ └──────┘ ┴
src └──────────────┘ └─────────────┘ └──────┘
typ └──────────────┘ └─────────────┘ └──────┘ ┴
doc └──────┘
565 @quotient (Π i ∈ l, α i) (by apply_instance))
id └──────┘ ┴ ┴ ┴ ┴
src └──────┘ └────────────┘
typ └──────┘ ┴ ┴ ┴ ┴ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
st └─────────────┘
566 finset.univ.1
id └─────────┘┴
src └─────────┘┴
typ └─────────┘┴
doc └─────────┘
567 (λ l, quotient.fin_choice_aux l (λ i _, f i))
id ┴ └─────────────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────────────────────┘
typ ┴ └─────────────────────┘ ┴ ┴ ┴ ┴ ┴
568 (λ a b h, begin
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └─────
569 have := λ a, quotient.fin_choice_aux_eq a (λ i h, quotient.out (f i)),
id └────────────────────────┘ └──────────┘ ┴
src └──────┘ └──┘└────────────────────────┘┴ ┴ └────┘└──────────┘┴ ┴ └┘
typ └──────┘ └──┘└────────────────────────┘┴ ┴ └────┘└──────────┘┴ ┴┴ └┘
doc └──────┘ └──┘ ┴ ┴ └────┘└──────────┘┴ ┴ └┘
txt └──────┘ └──┘ ┴ ┴ └────┘ ┴ ┴ └┘
par └──────┘ └──┘ ┴ ┴ └────┘ ┴ ┴ └┘
pid └───┘└─┘ └──┘ ┴ ┴ └────┘ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────┘└─
570 simp [quotient.out_eq] at this,
id └─────────────┘
src └────┘└─────────────┘└───────┘
typ └────┘└─────────────┘└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴┴ ┴┴└─────┘
st ───────────────────────────────────┘└─
571 simp [this],
id └──┘
src └────┘ ┴
typ └────┘└──┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ────────────────┘└─
572 let g := λ a:multiset ι, ⟦λ (i : ι) (h : i ∈ a), quotient.out (f i)⟧,
id └──────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴
src └───────┘ └─┘└──────┘┴ └┘┴ └────┘ └─────┘ ┴┴┴ └─┘└──────────┘┴ ┴ ┴┴
typ └───────┘ └─┘└──────┘┴ └┘┴ └────┘┴└─────┘ ┴┴┴ └─┘└──────────┘┴ ┴┴ ┴┴
doc └───────┘ └─┘└──────┘┴ └┘ └────┘ └─────┘ ┴ ┴ └─┘└──────────┘┴ ┴ ┴
txt └───────┘ └─┘ ┴ └┘ └────┘ └─────┘ ┴ ┴ └─┘ ┴ ┴ ┴
par └───────┘ └─┘ ┴ └┘ └────┘ └─────┘ ┴ ┴ └─┘ ┴ ┴ ┴
pid └───┘┴└─┘ └─┘ ┴ └┘ └────┘ └─────┘ ┴ ┴ └─┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────┘└─
573 refine eq_of_heq ((eq_rec_heq _ _).trans (_ : g a == g b)),
id └───────┘ └────────┘ ┴ └┘ ┴ ┴
src └─────┘└───────┘┴ └────────┘└──────────┘ └──┘ ┴ ┴└┘┴ ┴ └┘
typ └─────┘└───────┘┴ └────────┘└──────────┘ └──┘ ┴┴┴└┘┴┴┴┴└┘
doc └─────┘ ┴ └──────────┘ └──┘ ┴ ┴ ┴ ┴ └┘
txt └─────┘ ┴ └──────────┘ └──┘ ┴ ┴ ┴ ┴ └┘
par └─────┘ ┴ └──────────┘ └──┘ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ └──────────┘ └──┘ ┴ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────────┘└─
574 congr' 1, exact quotient.sound h,
id └────────────┘ ┴
src └──────┘ └────┘└────────────┘┴
typ └──────┘ └────┘└────────────┘┴┴
doc └──────┘ └────┘ ┴
txt └──────┘ └────┘ ┴
par └──────┘ └────┘ ┴
pid ┴┴ ┴ ┴
st ─────────────┘└──────────────────────┘└─
575 end))
st ──────┘
576 (λ f, ⟦λ i, f i (finset.mem_univ _)⟧)
id ┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴
src ┴ └─────────────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴
577 (λ a b h, quotient.sound $ λ i, h _ _)
id ┴ ┴ ┴ └────────────┘ ┴ ┴
src └────────────┘
typ ┴ ┴ ┴ └────────────┘ ┴ ┴
578
579 theorem quotient.fin_choice_eq {ι : Type*} [fintype ι] [decidable_eq ι]
id └─────┘ ┴ └──────────┘ ┴
src └─────┘ └──────────┘
typ └─────┘ ┴ └──────────┘ ┴
doc └─────┘
580 {α : ι → Type*} [∀ i, setoid (α i)]
id ┴ ┴ └────┘ ┴ ┴
src └────┘
typ ┴ ┴ └────┘ ┴ ┴
581 (f : ∀ i, α i) : quotient.fin_choice (λ i, ⟦f i⟧) = ⟦f⟧ :=
id ┴ ┴ ┴ └─────────────────┘ ┴ ┴┴ ┴┴ ┴ ┴┴┴
src └─────────────────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └─────────────────┘ ┴ ┴┴ ┴┴ ┴ ┴┴┴
582 begin
st └─────
583 let q, swap, change quotient.lift_on q _ _ = _,
id └──────────────┘ ┴ ┴
src └───┘ └──┘ └─────┘└──────────────┘┴ └───┘┴└┘
typ └───┘ └──┘ └─────┘└──────────────┘┴┴└───┘┴└┘
doc └───┘ └──┘ └─────┘ ┴ └───┘ └┘
txt └───┘ └──┘ └─────┘ ┴ └───┘ └┘
par └───┘ └──┘ └─────┘ ┴ └───┘ └┘
pid └───┘ ┴ ┴ └───┘ └┘
st ──────┘└────┘└─────────────────────────────────┘└─
584 have : q = ⟦λ i h, f i⟧,
id ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴┴ └────┘ ┴ ┴
typ └─────┘┴┴ ┴┴ └────┘┴┴ ┴
doc └─────┘ ┴ ┴ └────┘ ┴
txt └─────┘ ┴ ┴ └────┘ ┴
par └─────┘ ┴ ┴ └────┘ ┴
pid └───┘└┘ ┴ ┴ └────┘ ┴
st ────────────────────────┘└─
585 { dsimp [q],
id ┴
src └─────┘ ┴
typ └─────┘┴┴
doc └─────┘ ┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st ───┘└───────┘└─
586 exact quotient.induction_on
id └───────────────────┘
src └────┘└───────────────────┘└
typ └────┘└───────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ────────────────────────────────
587 (@finset.univ ι _).1 (λ l, quotient.fin_choice_aux_eq _ _) },
id └─────────┘ ┴ └────────────────────────┘
src ─────┘ └─────────┘┴ └────┘ └──┘└────────────────────────┘└────┘
typ ─────┘ └─────────┘┴┴└────┘ └──┘└────────────────────────┘└────┘
doc ─────┘ └─────────┘┴ └────┘ └──┘ └────┘
txt ─────┘ ┴ └────┘ └──┘ └────┘
par ─────┘ ┴ └────┘ └──┘ └────┘
pid ─────┘ ┴ └────┘ └──┘ └───┘┴
st ────────────────────────────────────────────────────────────────┘└┘└
588 simp [this], exact setoid.refl _
id └──┘ └─────────┘
src └────┘ ┴ └────┘└─────────┘└─┘
typ └────┘└──┘┴ └────┘└─────────┘└─┘
doc └────┘ ┴ └────┘ └─┘
txt └────┘ ┴ └────┘ └─┘
par └────┘ ┴ └────┘ └─┘
pid ┴┴ ┴ ┴ └┘┴
st ────────────┘└────────────────────┘
589 end
st └─┘
590
591 @[simp, to_additive]
doc └──┘ └─────────┘
592 lemma finset.prod_attach_univ [fintype α] [comm_monoid β] (f : {a : α // a ∈ @univ α _} → β) :
id └─────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └─────┘ └─────────┘ ┴ ┴ └──┘
typ └─────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc └─────┘ └──┘
593 univ.attach.prod (λ x, f x) = univ.prod (λ x, f ⟨x, (mem_univ _)⟩) :=
id └──┘└─────┘└───┘ ┴ ┴ ┴ ┴ └──┘└───┘ ┴ ┴ ┴ └──────┘
src └──┘└─────┘└───┘ ┴ └──┘└───┘ └──────┘
typ └──┘└─────┘└───┘ ┴ ┴ ┴ ┴ └──┘└───┘ ┴ ┴ ┴ └──────┘
doc └──┘└─────┘└───┘ └──┘└───┘
594 prod_bij (λ x _, x.1) (λ _ _, mem_univ _) (λ _ _ , by simp) (by simp) (λ b _, ⟨⟨b, mem_univ _⟩, by simp⟩)
id └──────┘ ┴ ┴ ┴┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └──────┘
src └──────┘ ┴ └──────┘ └──┘ └──┘ └──────┘ └──┘
typ └──────┘ ┴ ┴ ┴┴ ┴ ┴ └──────┘ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ └──────┘ └──┘
doc └──┘ └──┘ └──┘
txt └──┘ └──┘ └──┘
par └──┘ └──┘ └──┘
st └───┘ └───┘ └───┘
595
596 @[to_additive]
doc └─────────┘
597 lemma finset.range_prod_eq_univ_prod [comm_monoid β] (n : ℕ) (f : ℕ → β) :
id └─────────┘ ┴ ┴ ┴ ┴
src └─────────┘ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴
598 (range n).prod f = univ.prod (λ (k : fin n), f k) :=
id └───┘ ┴ └──┘ ┴ ┴ └──┘└───┘ └─┘ ┴ ┴ ┴
src └───┘ └──┘ ┴ └──┘└───┘ └─┘
typ └───┘ ┴ └──┘ ┴ ┴ └──┘└───┘ └─┘ ┴ ┴ ┴
doc └───┘ └──┘ └──┘└───┘
599 begin
st └─────
600 symmetry,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
st ─────────┘└─
601 refine prod_bij (λ k hk, k) _ _ _ _,
id └──────┘
src └─────┘└──────┘┴ └─────┘ └───────┘
typ └─────┘└──────┘┴ └─────┘ └───────┘
doc └─────┘ ┴ └─────┘ └───────┘
txt └─────┘ ┴ └─────┘ └───────┘
par └─────┘ ┴ └─────┘ └───────┘
pid ┴ ┴ └─────┘ └───────┘
st ────────────────────────────────────┘└─
602 { rintro ⟨k, hk⟩ _, simp * },
src └──────────────┘ └─────┘
typ └──────────────┘ └─────┘
doc └──────────────┘ └─────┘
txt └──────────────┘ └─────┘
par └──────────────┘ └─────┘
pid └────────┘ ┴┴┴
st ───┘└──────────────┘└───────┘└┘└
603 { rintro ⟨k, hk⟩ _, simp * },
src └──────────────┘ └─────┘
typ └──────────────┘ └─────┘
doc └──────────────┘ └─────┘
txt └──────────────┘ └─────┘
par └──────────────┘ └─────┘
pid └────────┘ ┴┴┴
st ───┘└──────────────┘└───────┘└┘└
604 { intros, rwa fin.eq_iff_veq },
id └────────────┘
src └────┘ └──┘└────────────┘┴
typ └────┘ └──┘└────────────┘┴
doc └────┘ └──┘ ┴
txt └────┘ └──┘ ┴
par └────┘ └──┘ ┴
pid ┴ ┴
st ───┘└────┘└───────────────────┘└┘└
605 { intros k hk, rw mem_range at hk,
id └───────┘
src └─────────┘ └─┘└───────┘└────┘
typ └─────────┘ └─┘└───────┘└────┘
doc └─────────┘ └─┘ └────┘
txt └─────────┘ └─┘ └────┘
par └─────────┘ └─┘ └────┘
pid └───┘ ┴ └────┘
st ──────────────┘└──────────────────┘└─
606 exact ⟨⟨k, hk⟩, mem_univ _, rfl⟩ }
id ┴ └┘ └──────┘ └─┘
src └────┘ └┘ └─┘└──────┘└──┘└─┘└┘
typ └────┘ ┴└┘└┘└─┘└──────┘└──┘└─┘└┘
doc └────┘ └┘ └─┘ └──┘ └┘
txt └────┘ └┘ └─┘ └──┘ └┘
par └────┘ └┘ └─┘ └──┘ └┘
pid ┴ └┘ └─┘ └──┘ ┴┴
st ────────────────────────────────────┘└─
607 end
st ──┘
608
609 section equiv
610
611 open list equiv equiv.perm
612
613 variables [decidable_eq α] [decidable_eq β]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
614
615 def perms_of_list : list α → list (perm α)
id └──┘ ┴ ┴ └──┘ └──┘ ┴
src └──┘ └──┘ └──┘
typ └──┘ ┴ ┴ └──┘ └──┘ ┴
doc └──┘
616 | [] := [1]
id └┘ ┴ ┴
src └┘ ┴ ┴
typ └┘ ┴ ┴
617 | (a :: l) := perms_of_list l ++ l.bind (λ b, (perms_of_list l).map (λ f, swap a b * f))
id ┴ └┘ ┴ └───────────┘ └┘ └───┘ ┴ └───────────┘ └─┘ ┴ └──┘ ┴ ┴ ┴
src └┘ └┘ └───┘ └─┘ └──┘ ┴
typ ┴ └┘ ┴ └───────────┘ └┘ └───┘ ┴ └───────────┘ └─┘ ┴ └──┘ ┴ ┴ ┴
doc └──┘
618
619 lemma length_perms_of_list : ∀ l : list α, length (perms_of_list l) = l.length.fact
id ┴ └──┘ ┴ └────┘ └───────────┘ ┴ ┴ ┴└─────┘└───┘
src └──┘ └────┘ └───────────┘ ┴ └─────┘└───┘
typ ┴ └──┘ ┴ └────┘ └───────────┘ ┴ ┴ ┴└─────┘└───┘
doc └───┘
620 | [] := rfl
id └┘ └─┘
src └┘ └─┘
typ └┘ └─┘
621 | (a :: l) := by rw [length_cons, nat.fact_succ];
id └┘ └─────────┘ └───────────┘
src └┘ └──┘└─────────┘└┘└───────────┘┴
typ └┘ └──┘└─────────┘└┘└───────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └──────────────┘└─────────────┘┴└─
622 simp [perms_of_list, length_bind, length_perms_of_list, function.comp, nat.succ_mul]
id └───────────┘ └─────────┘ └──────────────────┘ └───────────┘ └──────────┘
src └────┘└───────────┘└┘└─────────┘└┘ └┘└───────────┘└┘└──────────┘└─
typ └────┘└───────────┘└┘└─────────┘└┘└──────────────────┘└┘└───────────┘└┘└──────────┘└─
doc └────┘ └┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └┘ └┘ ┴└
st ───────────────────────────────────────────────────────────────────────────────────────
623
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
624 lemma mem_perms_of_list_of_mem : ∀ {l : list α} {f : perm α} (h : ∀ x, f x ≠ x → x ∈ l), f ∈ perms_of_list l
id ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴
src └──┘ └──┘ ┴ ┴ ┴ └───────────┘
typ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴
doc └──┘
625 | [] f h := list.mem_singleton.2 $ equiv.ext _ _$ λ x, by simp [imp_false, *] at *
id └┘ └────────────────┘┴ └───────┘ ┴ └───────┘
src └┘ └────────────────┘┴ └───────┘ └────┘└───────┘└────────┘
typ └┘ └────────────────┘┴ └───────┘ ┴ └────┘└───────┘└────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴┴ └──┘┴└──┘┴
st └────────────────────────┘
626 | (a::l) f h :=
id ┴└┘┴ ┴ ┴
src └┘
typ ┴└┘┴ ┴ ┴
627 if hfa : f a = a
id └┘ ┴
src └┘ ┴
typ └┘ ┴
628 then
629 mem_append_left _ $ mem_perms_of_list_of_mem
id └─────────────┘ └──────────────────────┘
src └─────────────┘
typ └─────────────┘ └──────────────────────┘
630 (λ x hx, mem_of_ne_of_mem (λ h, by rw h at hx; exact hx hfa) (h x hx))
id ┴ └┘ └──────────────┘ ┴ ┴ └┘ └─┘ ┴ └┘
src └──────────────┘ └─┘ └────┘ └────┘ ┴
typ ┴ └┘ └──────────────┘ ┴ └─┘┴└────┘ └────┘└┘┴└─┘ ┴ └┘
doc └─┘ └────┘ └────┘ ┴
txt └─┘ └────┘ └────┘ ┴
par └─┘ └────┘ └────┘ ┴
pid ┴ └────┘ ┴ ┴
st └───────────────────────┘
631 else
632 have hfa' : f (f a) ≠ f a, from mt (λ h, f.injective h) hfa,
id └──┘ ┴ └┘ ┴ └────────┘ ┴ └─┘
src ┴ └┘ └────────┘
typ └──┘ ┴ └┘ ┴ └────────┘ ┴ └─┘
633 have ∀ (x : α), (swap a (f a) * f) x ≠ x → x ∈ l,
id ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴ ┴
typ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
634 from λ x hx, have hxa : x ≠ a, from λ h, by simpa [h, mul_apply] using hx,
id ┴ └┘ ┴ ┴ ┴ ┴ └───────┘ └┘
src ┴ └─────┘ └┘└───────┘└──────┘
typ ┴ └┘ ┴ ┴ ┴ └─────┘┴└┘└───────┘└──────┘└┘
doc └─────┘ └┘ └──────┘
txt └─────┘ └┘ └──────┘
par └─────┘ └┘ └──────┘
pid ┴┴ └┘ ┴┴└────┘
st └────────────────────────────┘
635 have hfxa : f x ≠ f a, from mt (λ h, f.injective h) hxa,
id ┴ ┴ └┘ ┴ └────────┘ ┴ └─┘
src ┴ └┘ └────────┘
typ ┴ ┴ └┘ ┴ └────────┘ ┴ └─┘
636 list.mem_of_ne_of_mem hxa
id └───────────────────┘ └─┘
src └───────────────────┘
typ └───────────────────┘ └─┘
637 (h x (λ h, by simp [h, mul_apply, swap_apply_def] at hx; split_ifs at hx; cc)),
id ┴ ┴ ┴ └───────┘ └────────────┘
src └────┘ └┘└───────┘└┘└────────────┘└─────┘ └─────────────┘ └┘
typ ┴ ┴ └────┘┴└┘└───────┘└┘└────────────┘└─────┘ └─────────────┘ └┘
doc └────┘ └┘ └┘ └─────┘ └─────────────┘ └┘
txt └────┘ └┘ └┘ └─────┘ └─────────────┘ └┘
par └────┘ └┘ └┘ └─────┘ └─────────────┘ └┘
pid ┴┴ └┘ └┘ ┴┴└───┘ └────┘
st └─────────────────────────────────────────────────────────────┘
638 suffices f ∈ perms_of_list l ∨ ∃ (b : α), b ∈ l ∧ ∃ g : perm α, g ∈ perms_of_list l ∧ swap a b * g = f,
id ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴┴ ┴ ┴ └───────────┘ ┴ └──┘ ┴ ┴ ┴ ┴
src ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └───────────┘ ┴ └──┘ ┴ ┴
typ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴┴ ┴ ┴ └───────────┘ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘ └──┘
639 by simpa [perms_of_list],
id └───────────┘
src └─────┘└───────────┘┴
typ └─────┘└───────────┘┴
doc └─────┘ ┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴┴ ┴
st └────────────────────┘
640 (@or_iff_not_imp_left _ _ (classical.prop_decidable _)).2
id └─────────────────┘ └──────────────────────┘ ┴
src └─────────────────┘ └──────────────────────┘ ┴
typ └─────────────────┘ └──────────────────────┘ ┴
641 (λ hfl, ⟨f a,
id └─┘
typ └─┘
642 if hffa : f (f a) = a then mem_of_ne_of_mem hfa (h _ (mt (λ h, f.injective h) hfa))
id └┘ ┴ └──────────────┘ └─┘ └┘ ┴ └────────┘ ┴ └─┘
src └┘ ┴ └──────────────┘ └┘ └────────┘
typ └┘ ┴ └──────────────┘ └─┘ └┘ ┴ └────────┘ ┴ └─┘
643 else this _ $ by simp [mul_apply, swap_apply_def]; split_ifs; cc,
id └──┘ ┴ └───────┘ └────────────┘
src └────┘└───────┘└┘└────────────┘┴ └───────┘ └┘
typ └──┘ ┴ └────┘└───────┘└┘└────────────┘┴ └───────┘ └┘
doc └────┘ └┘ ┴ └───────┘ └┘
txt └────┘ └┘ ┴ └───────┘ └┘
par └────┘ └┘ ┴ └───────┘ └┘
pid ┴┴ └┘ ┴
st └──────────────────────────────────────────────┘
644 ⟨swap a (f a) * f, mem_perms_of_list_of_mem this,
id └──┘ ┴ └──────────────────────┘ └──┘
src └──┘ ┴
typ └──┘ ┴ └──────────────────────┘ └──┘
doc └──┘
645 by rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← equiv.perm.one_def, one_mul]⟩⟩)
id └───────┘ └─────┘ └──┘ ┴ ┴ └───────┘ └────────────────┘ └─────┘
src └────┘└───────┘└┘└─────┘┴ ┴ ┴ ┴ └─┘ └──┘┴ ┴ ┴ └──┘└───────┘└──┘└────────────────┘└┘└─────┘┴
typ └────┘└───────┘└┘└─────┘┴ ┴ ┴ ┴ └─┘ └──┘┴ ┴ ┴┴┴└──┘└───────┘└──┘└────────────────┘└┘└─────┘┴
doc └────┘ └┘ ┴ ┴ ┴ ┴ └─┘ └──┘┴ ┴ ┴ └──┘ └──┘ └┘ ┴
txt └────┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──┘ └──┘ └┘ ┴
par └────┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──┘ └──┘ └┘ ┴
pid └──┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──┘ └──┘ └┘ ┴
st └──────────────┘└─────────────────────────────────────┘└─────────┘└────────────────────┘└───────┘┴
646
647 lemma mem_of_mem_perms_of_list : ∀ {l : list α} {f : perm α}, f ∈ perms_of_list l → ∀ {x}, f x ≠ x → x ∈ l
id ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └──┘ ┴ └───────────┘ ┴ ┴
typ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
648 | [] f h := have f = 1 := by simpa [perms_of_list] using h, by rw this; simp
id └┘ ┴ ┴ └───────────┘ ┴ └──┘
src └┘ ┴ └─────┘└───────────┘└──────┘ └─┘ └───┘
typ └┘ ┴ ┴ └─────┘└───────────┘└──────┘┴ └─┘└──┘ └───┘
doc └─────┘ └──────┘ └─┘ └───┘
txt └─────┘ └──────┘ └─┘ └───┘
par └─────┘ └──────┘ └─┘ └───┘
pid ┴┴ ┴┴└────┘ ┴ ┴
st └────────────────────────────┘ └─────────────┘
649 | (a::l) f h :=
id ┴└┘ ┴
src └┘
typ ┴└┘ ┴
650 (mem_append.1 h).elim
id └────────┘┴ └──┘
src └────────┘┴ └──┘
typ └────────┘┴ └──┘
651 (λ h x hx, mem_cons_of_mem _ (mem_of_mem_perms_of_list h hx))
id ┴ ┴ └┘ └─────────────┘ └──────────────────────┘ ┴ └┘
src └─────────────┘
typ ┴ ┴ └┘ └─────────────┘ └──────────────────────┘ ┴ └┘
652 (λ h x hx,
id ┴ ┴ └┘
typ ┴ ┴ └┘
653 let ⟨y, hy, hy'⟩ := list.mem_bind.1 h in
id └─┘ ┴ └─┘ └───────────┘┴ ┴
src └───────────┘┴
typ └─┘ ┴ └─┘ └───────────┘┴ ┴
654 let ⟨g, hg₁, hg₂⟩ := list.mem_map.1 hy' in
id └─┘ └─┘ └──────────┘┴
src └──────────┘┴
typ └─┘ └─┘ └──────────┘┴
655 if hxa : x = a then by simp [hxa]
id └┘ ┴ ┴ └─┘
src └┘ ┴ └────┘ └─
typ └┘ ┴ ┴ └────┘└─┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
656 else if hxy : x = y then mem_cons_of_mem _ $ by rwa hxy
id └┘ ┴ ┴ └─────────────┘ └─┘
src ───┘ └┘ ┴ └─────────────┘ └──┘ └
typ ───┘ └┘ ┴ ┴ └─────────────┘ └──┘└─┘└
doc ───┘ └──┘ └
txt ───┘ └──┘ └
par ───┘ └──┘ └
pid ───┘ ┴ └
st ───┘ └────────
657 else mem_cons_of_mem _ $
id └─────────────┘ ┴
src ───┘ └─────────────┘
typ ───┘ └─────────────┘ ┴
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘
658 mem_of_mem_perms_of_list hg₁ $
id └──────────────────────┘
typ └──────────────────────┘
659 by rw [eq_inv_mul_iff_mul_eq.2 hg₂, mul_apply, swap_inv, swap_apply_def];
id └───────────────────┘ └─┘ └───────┘ └──────┘ └────────────┘
src └──┘└───────────────────┘└─┘ └┘└───────┘└┘└──────┘└┘└────────────┘┴
typ └──┘└───────────────────┘└─┘└─┘└┘└───────┘└┘└──────┘└┘└────────────┘┴
doc └──┘ └─┘ └┘ └┘ └┘ ┴
txt └──┘ └─┘ └┘ └┘ └┘ ┴
par └──┘ └─┘ └┘ └┘ └┘ ┴
pid └┘ └─┘ └┘ └┘ └┘ ┴
st └──────────────────────────────┘└─────────┘└────────┘└──────────────┘┴└─
660 split_ifs; cc)
src └───────┘ └┘
typ └───────┘ └┘
doc └───────┘ └┘
txt └───────┘ └┘
par └───────┘ └┘
st ────────────────────┘
661
662 lemma mem_perms_of_list_iff {l : list α} {f : perm α} : f ∈ perms_of_list l ↔ ∀ {x}, f x ≠ x → x ∈ l :=
id └──┘ ┴ └──┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └──┘ ┴ └───────────┘ ┴ ┴ ┴
typ └──┘ ┴ └──┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
663 ⟨mem_of_mem_perms_of_list, mem_perms_of_list_of_mem⟩
id └──────────────────────┘ └──────────────────────┘
src └──────────────────────┘ └──────────────────────┘
typ └──────────────────────┘ └──────────────────────┘
664
665 lemma nodup_perms_of_list : ∀ {l : list α} (hl : l.nodup), (perms_of_list l).nodup
id ┴ └──┘ ┴ ┴└────┘ └───────────┘ ┴ └───┘
src └──┘ └────┘ └───────────┘ └───┘
typ ┴ └──┘ ┴ ┴└────┘ └───────────┘ ┴ └───┘
doc └────┘ └───┘
666 | [] hl := by simp [perms_of_list]
id └┘ └───────────┘
src └┘ └────┘└───────────┘└┘
typ └┘ └────┘└───────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └────────────────────┘
667 | (a::l) hl :=
id ┴└┘┴ └┘
src └┘
typ ┴└┘┴ └┘
668 have hl' : l.nodup, from nodup_of_nodup_cons hl,
id └────┘ └─────────────────┘
src └────┘ └─────────────────┘
typ └────┘ └─────────────────┘
doc └────┘
669 have hln' : (perms_of_list l).nodup, from nodup_perms_of_list hl',
id └───────────┘ └───┘ └─────────────────┘ └─┘
src └───────────┘ └───┘
typ └───────────┘ └───┘ └─────────────────┘ └─┘
doc └───┘
670 have hmeml : ∀ {f : perm α}, f ∈ perms_of_list l → f a = a,
id └──┘ ┴ ┴ ┴ └───────────┘ ┴ ┴
src └──┘ ┴ └───────────┘ ┴
typ └──┘ ┴ ┴ ┴ └───────────┘ ┴ ┴
doc └──┘
671 from λ f hf, not_not.1 (mt (mem_of_mem_perms_of_list hf) (nodup_cons.1 hl).1),
id ┴ └┘ └─────┘┴ └┘ └──────────────────────┘ └┘ └────────┘┴ ┴
src └─────┘┴ └┘ └──────────────────────┘ └────────┘┴ ┴
typ ┴ └┘ └─────┘┴ └┘ └──────────────────────┘ └┘ └────────┘┴ ┴
672 by rw [perms_of_list, list.nodup_append, list.nodup_bind, pairwise_iff_nth_le]; exact
id └───────────┘ └───────────────┘ └─────────────┘ └─────────────────┘
src └──┘└───────────┘└┘└───────────────┘└┘└─────────────┘└┘└─────────────────┘┴ └────┘
typ └──┘└───────────┘└┘└───────────────┘└┘└─────────────┘└┘└─────────────────┘┴ └────┘
doc └──┘ └┘ └┘ └┘ ┴ └────┘
txt └──┘ └┘ └┘ └┘ ┴ └────┘
par └──┘ └┘ └┘ └┘ ┴ └────┘
pid └┘ └┘ └┘ └┘ ┴ ┴
st └────────────────┘└─────────────────┘└───────────────┘└───────────────────┘┴└───────
673 ⟨hln', ⟨λ _ _, nodup_map (λ _ _, (mul_left_inj _).1) hln',
id └───────┘ └──────────┘ └──┘
src └┘ └────┘└───────┘┴ └────┘ └──────────┘└─────┘ └─
typ └┘ └────┘└───────┘┴ └────┘ └──────────┘└─────┘└──┘└─
doc └┘ └────┘ ┴ └────┘ └─────┘ └─
txt └┘ └────┘ ┴ └────┘ └─────┘ └─
par └┘ └────┘ ┴ └────┘ └─────┘ └─
pid └┘ └────┘ ┴ └────┘ └─────┘ └─
st ───────────────────────────────────────────────────────────
674 λ i j hj hij x hx₁ hx₂,
src ─┘ └──────────────────────
typ ─┘ └──────────────────────
doc ─┘ └──────────────────────
txt ─┘ └──────────────────────
par ─┘ └──────────────────────
pid ─┘ └──────────────────────
st ──────────────────────────
675 let ⟨f, hf⟩ := list.mem_map.1 hx₁ in
id └┘
src ───┘ ┴ └┘ └───┘ └─┘ └───
typ ───┘ ┴ └┘└┘└───┘ └─┘ └───
doc ───┘ ┴ └┘ └───┘ └─┘ └───
txt ───┘ ┴ └┘ └───┘ └─┘ └───
par ───┘ ┴ └┘ └───┘ └─┘ └───
pid ───┘ ┴ └┘ └───┘ └─┘ └───
st ─────────────────────────────────────────
676 let ⟨g, hg⟩ := list.mem_map.1 hx₂ in
id └┘
src ───┘ ┴ └┘ └───┘ └─┘ └───
typ ───┘ ┴ └┘└┘└───┘ └─┘ └───
doc ───┘ ┴ └┘ └───┘ └─┘ └───
txt ───┘ ┴ └┘ └───┘ └─┘ └───
par ───┘ ┴ └┘ └───┘ └─┘ └───
pid ───┘ ┴ └┘ └───┘ └─┘ └───
st ─────────────────────────────────────────
677 have hix : x a = nth_le l i (lt_trans hij hj),
id ┴ ┴ └┘
src ───┘ └─────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ └──
typ ───┘ └─────┘ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴└┘└──
doc ───┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
txt ───┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
par ───┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
pid ───┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
st ───────────────────────────────────────────────────
678 by rw [← hf.2, mul_apply, hmeml hf.1, swap_apply_left],
id └┘ └───────┘ └───┘ └┘ └─────────────┘
src ────────┘└────┘ └──┘└───────┘└┘ ┴ └──┘└─────────────┘┴└─
typ ────────┘└────┘└┘└──┘└───────┘└┘└───┘┴└┘└──┘└─────────────┘┴└─
doc ────────┘└────┘ └──┘ └┘ ┴ └──┘ ┴└─
txt ────────┘└────┘ └──┘ └┘ ┴ └──┘ ┴└─
par ────────┘└────┘ └──┘ └┘ ┴ └──┘ ┴└─
pid ──────────────┘ └──┘ └┘ ┴ └──┘ └──
st ───────┘└───────┘└───────────┘└────────┘└─────────────────┘┴└─
679 have hiy : x a = nth_le l j hj,
id └────┘ ┴ └┘
src ───┘ └─────┘ ┴ ┴ ┴└────┘┴ ┴ ┴ └─
typ ───┘ └─────┘ ┴ ┴ ┴└────┘┴┴┴ ┴└┘└─
doc ───┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
txt ───┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
par ───┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid ───┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
st ────────────────────────────────────
680 by rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left],
id └┘ └───────┘ └───┘ └┘ └─────────────┘
src ────────┘└────┘ └──┘└───────┘└┘ ┴ └──┘└─────────────┘┴└─
typ ────────┘└────┘└┘└──┘└───────┘└┘└───┘┴└┘└──┘└─────────────┘┴└─
doc ────────┘└────┘ └──┘ └┘ ┴ └──┘ ┴└─
txt ────────┘└────┘ └──┘ └┘ ┴ └──┘ ┴└─
par ────────┘└────┘ └──┘ └┘ ┴ └──┘ ┴└─
pid ──────────────┘ └──┘ └┘ ┴ └──┘ └──
st ───────┘└───────┘└───────────┘└────────┘└─────────────────┘┴└─
681 absurd (hf.2.trans (hg.2.symm)) $
id └────┘
src ───┘└────┘┴ └───────┘ └────────┘ └
typ ───┘└────┘┴ └───────┘ └────────┘ └
doc ───┘ ┴ └───────┘ └────────┘ └
txt ───┘ ┴ └───────┘ └────────┘ └
par ───┘ ┴ └───────┘ └────────┘ └
pid ───┘ ┴ └───────┘ └────────┘ └
st ──────────────────────────────────────
682 λ h, ne_of_lt hij $ nodup_iff_nth_le_inj.1 hl' i j (lt_trans hij hj) hj $
id └──────┘ └──────────────────┘ └─┘ ┴ ┴ └──────┘ └┘
src ─────┘ └──┘└──────┘┴ ┴ ┴└──────────────────┘└─┘ ┴ ┴ ┴ └──────┘┴ ┴ └┘ ┴ └
typ ─────┘ └──┘└──────┘┴ ┴ ┴└──────────────────┘└─┘└─┘┴┴┴┴┴ └──────┘┴ ┴└┘└┘ ┴ └
doc ─────┘ └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └
txt ─────┘ └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └
par ─────┘ └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └
pid ─────┘ └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └
st ────────────────────────────────────────────────────────────────────────────────
683 by rw [← hix, hiy]⟩,
id └─┘ └─┘
src ───────┘ ┴└────┘ └┘ ┴└──
typ ───────┘ ┴└────┘└─┘└┘└─┘┴└──
doc ───────┘ ┴└────┘ └┘ ┴└──
txt ───────┘ ┴└────┘ └┘ ┴└──
par ───────┘ ┴└────┘ └┘ ┴└──
pid ───────┘ └─────┘ └┘ └───
st ─────────┘└────────┘└───┘┴└──
684 λ f hf₁ hf₂,
src ─┘ └───────────
typ ─┘ └───────────
doc ─┘ └───────────
txt ─┘ └───────────
par ─┘ └───────────
pid ─┘ └───────────
st ───────────────
685 let ⟨x, hx, hx'⟩ := list.mem_bind.1 hf₂ in
id ┴ └┘ └─┘ └───────────┘
src ───┘ ┴ └┘ └┘ └───┘└───────────┘└─┘ └───
typ ───┘ ┴ ┴└┘└┘└┘└─┘└───┘└───────────┘└─┘ └───
doc ───┘ ┴ └┘ └┘ └───┘ └─┘ └───
txt ───┘ ┴ └┘ └┘ └───┘ └─┘ └───
par ───┘ ┴ └┘ └┘ └───┘ └─┘ └───
pid ───┘ ┴ └┘ └┘ └───┘ └─┘ └───
st ───────────────────────────────────────────────
686 let ⟨g, hg⟩ := list.mem_map.1 hx' in
id ┴ └┘ └──────────┘
src ───┘ ┴ └┘ └───┘└──────────┘└─┘ └───
typ ───┘ ┴ ┴└┘└┘└───┘└──────────┘└─┘ └───
doc ───┘ ┴ └┘ └───┘ └─┘ └───
txt ───┘ ┴ └┘ └───┘ └─┘ └───
par ───┘ ┴ └┘ └───┘ └─┘ └───
pid ───┘ ┴ └┘ └───┘ └─┘ └───
st ─────────────────────────────────────────
687 have hgxa : g⁻¹ x = a, from f.injective $
id └┘ └────────┘
src ───┘ └──────┘ └┘┴ ┴ ┴ └─────┘ └────────┘┴ └
typ ───┘ └──────┘ └┘┴ ┴ ┴ └─────┘ └────────┘┴ └
doc ───┘ └──────┘ ┴ ┴ ┴ └─────┘ ┴ └
txt ───┘ └──────┘ ┴ ┴ ┴ └─────┘ ┴ └
par ───┘ └──────┘ ┴ ┴ ┴ └─────┘ ┴ └
pid ───┘ └──────┘ ┴ ┴ ┴ └─────┘ ┴ └
st ──────────────────────────────────────────────
688 by rw [hmeml hf₁, ← hg.2]; simp,
id └───┘ └─┘ └┘
src ─────┘ ┴└──┘ ┴ └──┘ └─┘└┘└──┘└─
typ ─────┘ ┴└──┘└───┘┴└─┘└──┘└┘└─┘└┘└──┘└─
doc ─────┘ ┴└──┘ ┴ └──┘ └─┘└┘└──┘└─
txt ─────┘ ┴└──┘ ┴ └──┘ └─┘└┘└──┘└─
par ─────┘ ┴└──┘ ┴ └──┘ └─┘└┘└──┘└─
pid ─────┘ └───┘ ┴ └──┘ └──────────
st ───────┘└────────────┘└────┘└─┘└────┘└─
689 have hxa : x ≠ a, from λ h, (list.nodup_cons.1 hl).1 (h ▸ hx),
id ┴ ┴ └─────────────┘ └┘
src ───┘ └─────┘ ┴┴┴ └─────┘ └──┘ └─────────────┘└─┘ └──┘ ┴ ┴ └──
typ ───┘ └─────┘ ┴┴┴┴└─────┘ └──┘ └─────────────┘└─┘└┘└──┘ ┴ ┴ └──
doc ───┘ └─────┘ ┴ ┴ └─────┘ └──┘ └─┘ └──┘ ┴ ┴ └──
txt ───┘ └─────┘ ┴ ┴ └─────┘ └──┘ └─┘ └──┘ ┴ ┴ └──
par ───┘ └─────┘ ┴ ┴ └─────┘ └──┘ └─┘ └──┘ ┴ ┴ └──
pid ───┘ └─────┘ ┴ ┴ └─────┘ └──┘ └─┘ └──┘ ┴ ┴ └──
st ───────────────────────────────────────────────────────────────────
690 (list.nodup_cons.1 hl).1 $
src ───┘ └─┘ └──┘ └
typ ───┘ └─┘ └──┘ └
doc ───┘ └─┘ └──┘ └
txt ───┘ └─┘ └──┘ └
par ───┘ └─┘ └──┘ └
pid ───┘ └─┘ └──┘ └
st ───────────────────────────────
691 hgxa ▸ mem_of_mem_perms_of_list hg.1 (by rwa [apply_inv_self, hgxa])⟩
id ┴ └──────────────────────┘ └────────────┘ └──┘
src ─────┘ ┴┴┴└──────────────────────┘┴ └─┘ ┴└───┘└────────────┘└┘ ┴└──
typ ─────┘ ┴┴┴└──────────────────────┘┴ └─┘ ┴└───┘└────────────┘└┘└──┘┴└──
doc ─────┘ ┴ ┴ ┴ └─┘ ┴└───┘ └┘ ┴└──
txt ─────┘ ┴ ┴ ┴ └─┘ ┴└───┘ └┘ ┴└──
par ─────┘ ┴ ┴ ┴ └─┘ ┴└───┘ └┘ ┴└──
pid ─────┘ ┴ ┴ ┴ └─┘ └────┘ └┘ └─┘└
st ─────────────────────────────────────────────┘└──────────────────┘└────┘┴└──
692
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
693 def perms_of_finset (s : finset α) : finset (perm α) :=
id └────┘ ┴ └────┘ └──┘ ┴
src └────┘ └────┘ └──┘
typ └────┘ ┴ └────┘ └──┘ ┴
doc └────┘ └────┘ └──┘
694 quotient.hrec_on s.1 (λ l hl, ⟨perms_of_list l, nodup_perms_of_list hl⟩)
id └──────────────┘ ┴┴ ┴ └┘ └───────────┘ ┴ └─────────────────┘ └┘
src └──────────────┘ ┴ └───────────┘ └─────────────────┘
typ └──────────────┘ ┴┴ ┴ └┘ └───────────┘ ┴ └─────────────────┘ └┘
695 (λ a b hab, hfunext (congr_arg _ (quotient.sound hab))
id ┴ ┴ └─┘ └─────┘ └───────┘ └────────────┘ └─┘
src └─────┘ └───────┘ └────────────┘
typ ┴ ┴ └─┘ └─────┘ └───────┘ └────────────┘ └─┘
696 (λ ha hb _, heq_of_eq $ finset.ext.2 $
id └┘ └┘ ┴ └───────┘ └────────┘┴
src └───────┘ └────────┘┴
typ └┘ └┘ ┴ └───────┘ └────────┘┴
697 by simp [mem_perms_of_list_iff,mem_of_perm hab]))
id └───────────────────┘ └─────────┘ └─┘
src └────┘└───────────────────┘┴└─────────┘┴ ┴
typ └────┘└───────────────────┘┴└─────────┘┴└─┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴┴ ┴ ┴ ┴
st └───────────────────────────────────────────┘
698 s.2
id ┴┴
src ┴
typ ┴┴
699
700 lemma mem_perms_of_finset_iff : ∀ {s : finset α} {f : perm α},
id └────┘ ┴ └──┘ ┴
src └────┘ └──┘
typ └────┘ ┴ └──┘ ┴
doc └────┘ └──┘
701 f ∈ perms_of_finset s ↔ ∀ {x}, f x ≠ x → x ∈ s :=
id ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─────────────┘ ┴ ┴ ┴
typ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
702 by rintros ⟨⟨l⟩, hs⟩ f; exact mem_perms_of_list_iff
id └───────────────────┘
src └─────────────────┘ └────┘└───────────────────┘└
typ └─────────────────┘ └────┘└───────────────────┘└
doc └─────────────────┘ └────┘ └
txt └─────────────────┘ └────┘ └
par └─────────────────┘ └────┘ └
pid └──────────┘ ┴ └
st └─────────────────────────────────────────────────
703
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
704 lemma card_perms_of_finset : ∀ (s : finset α),
id └────┘ ┴
src └────┘
typ └────┘ ┴
doc └────┘
705 (perms_of_finset s).card = s.card.fact :=
id └─────────────┘ ┴ └──┘ ┴ ┴└───┘└───┘
src └─────────────┘ └──┘ ┴ └───┘└───┘
typ └─────────────┘ ┴ └──┘ ┴ ┴└───┘└───┘
doc └──┘ └───┘└───┘
706 by rintros ⟨⟨l⟩, hs⟩; exact length_perms_of_list l
id └──────────────────┘ ┴
src └───────────────┘ └────┘└──────────────────┘┴ └
typ └───────────────┘ └────┘└──────────────────┘┴┴└
doc └───────────────┘ └────┘ ┴ └
txt └───────────────┘ └────┘ ┴ └
par └───────────────┘ └────┘ ┴ └
pid └────────┘ ┴ ┴ └
st └────────────────────────────────────────────────
707
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
708 def fintype_perm [fintype α] : fintype (perm α) :=
id └─────┘ ┴ └─────┘ └──┘ ┴
src └─────┘ └─────┘ └──┘
typ └─────┘ ┴ └─────┘ └──┘ ┴
doc └─────┘ └─────┘ └──┘
709 ⟨perms_of_finset (@finset.univ α _), by simp [mem_perms_of_finset_iff]⟩
id └─────────────┘ └─────────┘ ┴ └─────────────────────┘
src └─────────────┘ └─────────┘ └────┘└─────────────────────┘┴
typ └─────────────┘ └─────────┘ ┴ └────┘└─────────────────────┘┴
doc └─────────┘ └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────────────────────────┘
710
711 instance [fintype α] [fintype β] : fintype (α ≃ β) :=
id └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
src └─────┘ └─────┘ └─────┘ ┴
typ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └─────┘ └─────┘ ┴
712 if h : fintype.card β = fintype.card α
id └┘ └──────────┘ ┴ ┴ └──────────┘ ┴
src └┘ └──────────┘ ┴ └──────────┘
typ └┘ └──────────┘ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘
713 then trunc.rec_on_subsingleton (fintype.equiv_fin α)
id └───────────────────────┘ └───────────────┘ ┴
src └───────────────────────┘ └───────────────┘
typ └───────────────────────┘ └───────────────┘ ┴
doc └───────────────┘
714 (λ eα, trunc.rec_on_subsingleton (fintype.equiv_fin β)
id └┘ └───────────────────────┘ └───────────────┘ ┴
src └───────────────────────┘ └───────────────┘
typ └┘ └───────────────────────┘ └───────────────┘ ┴
doc └───────────────┘
715 (λ eβ, @fintype.of_equiv _ (perm α) fintype_perm
id └┘ └──────────────┘ └──┘ ┴ └──────────┘
src └──────────────┘ └──┘ └──────────┘
typ └┘ └──────────────┘ └──┘ ┴ └──────────┘
doc └──────────────┘ └──┘
716 (equiv_congr (equiv.refl α) (eα.trans (eq.rec_on h eβ.symm)) : (α ≃ α) ≃ (α ≃ β))))
id └─────────┘ └────────┘ ┴ └┘└────┘ └───────┘ ┴ └┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────┘ └────────┘ └────┘ └───────┘ └───┘ ┴ ┴ ┴
typ └─────────┘ └────────┘ ┴ └┘└────┘ └───────┘ ┴ └┘└───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴
717 else ⟨∅, λ x, false.elim (h (fintype.card_eq.2 ⟨x.symm⟩))⟩
id ┴┴ ┴ └────────┘ ┴ └─────────────┘┴ ┴└───┘
src ┴ └────────┘ └─────────────┘┴ └───┘
typ ┴┴ ┴ └────────┘ ┴ └─────────────┘┴ ┴└───┘
718
719 lemma fintype.card_perm [fintype α] : fintype.card (perm α) = (fintype.card α).fact :=
id └─────┘ ┴ └──────────┘ └──┘ ┴ ┴ └──────────┘ ┴ └──┘
src └─────┘ └──────────┘ └──┘ ┴ └──────────┘ └──┘
typ └─────┘ ┴ └──────────┘ └──┘ ┴ ┴ └──────────┘ ┴ └──┘
doc └─────┘ └──────────┘ └──┘ └──────────┘ └──┘
720 subsingleton.elim (@fintype_perm α _ _) (@equiv.fintype α α _ _ _ _) ▸
id └───────────────┘ └──────────┘ ┴ └───────────┘ ┴ ┴ ┴
src └───────────────┘ └──────────┘ └───────────┘ ┴
typ └───────────────┘ └──────────┘ ┴ └───────────┘ ┴ ┴ ┴
721 card_perms_of_finset _
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
722
723 lemma fintype.card_equiv [fintype α] [fintype β] (e : α ≃ β) :
id └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
src └─────┘ └─────┘ ┴
typ └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘ ┴
724 fintype.card (α ≃ β) = (fintype.card α).fact :=
id └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ └──┘
src └──────────┘ ┴ ┴ └──────────┘ └──┘
typ └──────────┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ └──┘
doc └──────────┘ ┴ └──────────┘ └──┘
725 fintype.card_congr (equiv_congr (equiv.refl α) e) ▸ fintype.card_perm
id └────────────────┘ └─────────┘ └────────┘ ┴ ┴ ┴ └───────────────┘
src └────────────────┘ └─────────┘ └────────┘ ┴ └───────────────┘
typ └────────────────┘ └─────────┘ └────────┘ ┴ ┴ ┴ └───────────────┘
726
727 end equiv
728
729 namespace fintype
730
731 section choose
732 open fintype
733 open equiv
734
735 variables [fintype α] [decidable_eq α] (p : α → Prop) [decidable_pred p]
id └─────┘ └──────────┘ └────────────┘
src └─────┘ └──────────┘ └────────────┘
typ └─────┘ └──────────┘ └────────────┘
doc └─────┘
736
737 def choose_x (hp : ∃! a : α, p a) : {a // p a} :=
id └┘ ┴┴ ┴ ┴ ┴┴ ┴ ┴
src └┘ ┴ ┴
typ └┘ ┴┴ ┴ ┴ ┴┴ ┴ ┴
738 ⟨finset.choose p univ (by simp; exact hp), finset.choose_property _ _ _⟩
id └───────────┘ ┴ └──┘ └┘ └────────────────────┘
src └───────────┘ └──┘ └──┘ └────┘ └────────────────────┘
typ └───────────┘ ┴ └──┘ └──┘ └────┘└┘ └────────────────────┘
doc └──┘ └──┘ └────┘
txt └──┘ └────┘
par └──┘ └────┘
pid ┴
st └─────────────┘
739
740 def choose (hp : ∃! a, p a) : α := choose_x p hp
id └┘ ┴┴ ┴ ┴ ┴ └──────┘ ┴ └┘
src └┘ ┴ └──────┘
typ └┘ ┴┴ ┴ ┴ ┴ └──────┘ ┴ └┘
st ┴
741
742 lemma choose_spec (hp : ∃! a, p a) : p (choose p hp) :=
id └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ └┘
src └┘ ┴ └────┘
typ └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ └┘
743 (choose_x p hp).property
id └──────┘ ┴ └┘ └──────┘
src └──────┘ └──────┘
typ └──────┘ ┴ └┘ └──────┘
744
745 end choose
746
747 section bijection_inverse
748 open function
749
750 variables [fintype α] [decidable_eq α]
id └─────┘ └──────────┘
src └─────┘ └──────────┘
typ └─────┘ └──────────┘
doc └─────┘
751 variables [fintype β] [decidable_eq β]
id └─────┘ └──────────┘
src └─────┘ └──────────┘
typ └─────┘ └──────────┘
doc └─────┘
752 variables {f : α → β}
753
754 /-- `
755 `bij_inv f` is the unique inverse to a bijection `f`. This acts
756 as a computable alternative to `function.inv_fun`. -/
757 def bij_inv (f_bij : bijective f) (b : β) : α :=
id └───────┘ ┴ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴ ┴
758 fintype.choose (λ a, f a = b)
id └────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────┘ ┴
typ └────────────┘ ┴ ┴ ┴ ┴ ┴
759 begin
st └─────
760 rcases f_bij.right b with ⟨a', fa_eq_b⟩,
id └─────────┘ ┴
src └─────┘└─────────┘┴ └─────────────────┘
typ └─────┘└─────────┘┴┴└─────────────────┘
doc └─────┘ ┴ └─────────────────┘
txt └─────┘ ┴ └─────────────────┘
par └─────┘ ┴ └─────────────────┘
pid ┴ ┴ └─────────────────┘
st ────────────────────────────────────────┘└─
761 rw ← fa_eq_b,
id └─────┘
src └───┘
typ └───┘└─────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ─────────────┘└─
762 exact ⟨a', ⟨rfl, (λ a h, f_bij.left h)⟩⟩
id └┘ └─┘ └────────┘
src └────┘ └┘ └─┘└┘ └────┘└────────┘┴ └──┘
typ └────┘ └┘└┘ └─┘└┘ └────┘└────────┘┴ └──┘
doc └────┘ └┘ └┘ └────┘ ┴ └──┘
txt └────┘ └┘ └┘ └────┘ ┴ └──┘
par └────┘ └┘ └┘ └────┘ ┴ └──┘
pid ┴ └┘ └┘ └────┘ ┴ └─┘┴
st ──────────────────────────────────────────┘
763 end
st └─┘
764
765 lemma left_inverse_bij_inv (f_bij : bijective f) : left_inverse (bij_inv f_bij) f :=
id └───────┘ ┴ └──────────┘ └─────┘ └───┘ ┴
src └───────┘ └──────────┘ └─────┘
typ └───────┘ ┴ └──────────┘ └─────┘ └───┘ ┴
doc └─────┘
766 λ a, f_bij.left (choose_spec (λ a', f a' = f a) _)
id ┴ └───┘└───┘ └─────────┘ └┘ ┴ └┘ ┴ ┴ ┴
src └───┘ └─────────┘ ┴
typ ┴ └───┘└───┘ └─────────┘ └┘ ┴ └┘ ┴ ┴ ┴
767
768 lemma right_inverse_bij_inv (f_bij : bijective f) : right_inverse (bij_inv f_bij) f :=
id └───────┘ ┴ └───────────┘ └─────┘ └───┘ ┴
src └───────┘ └───────────┘ └─────┘
typ └───────┘ ┴ └───────────┘ └─────┘ └───┘ ┴
doc └─────┘
769 λ b, choose_spec (λ a', f a' = b) _
id ┴ └─────────┘ └┘ ┴ └┘ ┴ ┴
src └─────────┘ ┴
typ ┴ └─────────┘ └┘ ┴ └┘ ┴ ┴
770
771 lemma bijective_bij_inv (f_bij : bijective f) : bijective (bij_inv f_bij) :=
id └───────┘ ┴ └───────┘ └─────┘ └───┘
src └───────┘ └───────┘ └─────┘
typ └───────┘ ┴ └───────┘ └─────┘ └───┘
doc └─────┘
772 ⟨injective_of_left_inverse (right_inverse_bij_inv _),
id └───────────────────────┘ └───────────────────┘
src └───────────────────────┘ └───────────────────┘
typ └───────────────────────┘ └───────────────────┘
773 surjective_of_has_right_inverse ⟨f, left_inverse_bij_inv _⟩⟩
id └─────────────────────────────┘ ┴ └──────────────────┘
src └─────────────────────────────┘ └──────────────────┘
typ └─────────────────────────────┘ ┴ └──────────────────┘
774
775 end bijection_inverse
776
777 lemma well_founded_of_trans_of_irrefl [fintype α] (r : α → α → Prop)
id └─────┘ ┴ ┴ ┴
src └─────┘
typ └─────┘ ┴ ┴ ┴
doc └─────┘
778 [is_trans α r] [is_irrefl α r] : well_founded r :=
id └──────┘ ┴ ┴ └───────┘ ┴ ┴ └──────────┘ ┴
src └──────┘ └───────┘ └──────────┘
typ └──────┘ ┴ ┴ └───────┘ ┴ ┴ └──────────┘ ┴
779 by classical; exact
src └───────┘ └────┘
typ └───────┘ └────┘
doc └───────┘ └────┘
txt └───────┘ └────┘
par └───────┘ └────┘
pid ┴
st └─────────────────
780 have ∀ x y, r x y → (univ.filter (λ z, r z x)).card < (univ.filter (λ z, r z y)).card,
id ┴ ┴ └─────────┘ ┴
src ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──────┘┴┴ └─────────┘┴ └──┘ ┴ ┴ └────────
typ ┴ └──┘ ┴┴┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──────┘┴┴ └─────────┘┴ └──┘┴┴ ┴ └────────
doc ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──────┘ ┴ └─────────┘┴ └──┘ ┴ ┴ └────────
txt ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──────┘ ┴ ┴ └──┘ ┴ ┴ └────────
par ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──────┘ ┴ ┴ └──┘ ┴ ┴ └────────
pid ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──────┘ ┴ ┴ └──┘ ┴ ┴ └────────
st ───────────────────────────────────────────────────────────────────────────────────────
781 from λ x y hxy, finset.card_lt_card $
id └─────────────────┘
src ──────┘ └────────┘└─────────────────┘┴ └
typ ──────┘ └────────┘└─────────────────┘┴ └
doc ──────┘ └────────┘ ┴ └
txt ──────┘ └────────┘ ┴ └
par ──────┘ └────────┘ ┴ └
pid ──────┘ └────────┘ ┴ └
st ────────────────────────────────────────
782 by simp only [finset.lt_iff_ssubset.symm, lt_iff_le_not_le,
id └──────────────┘
src ───┘ ┴└─────────┘ └┘└──────────────┘└─
typ ───┘ ┴└─────────┘└────────────────────────┘└┘└──────────────┘└─
doc ───┘ ┴└─────────┘ └┘ └─
txt ───┘ ┴└─────────┘ └┘ └─
par ───┘ ┴└─────────┘ └┘ └─
pid ───┘ └──────────┘ └┘ └─
st ─────┘└─────────────────────────────────────────────────────────
783 finset.le_iff_subset, finset.subset_iff, mem_filter, true_and, mem_univ, hxy];
id └──────────────────┘ └───────────────┘ └────────┘ └──────┘ └──────┘ └─┘
src ─────┘└──────────────────┘└┘└───────────────┘└┘└────────┘└┘└──────┘└┘└──────┘└┘ ┴└─
typ ─────┘└──────────────────┘└┘└───────────────┘└┘└────────┘└┘└──────┘└┘└──────┘└┘└─┘┴└─
doc ─────┘ └┘ └┘ └┘ └┘ └┘ ┴└─
txt ─────┘ └┘ └┘ └┘ └┘ └┘ ┴└─
par ─────┘ └┘ └┘ └┘ └┘ └┘ ┴└─
pid ─────┘ └┘ └┘ └┘ └┘ └┘ └──
st ─────────────────────────────────────────────────────────────────────────────────────
784 exact ⟨λ z hzx, trans hzx hxy, not_forall_of_exists_not ⟨x, not_imp.2 ⟨hxy, irrefl x⟩⟩⟩,
id └───┘ └──────────────────────┘ └─────┘ └─┘ └────┘ ┴
src ─────────┘ └──────┘└───┘┴ ┴ └┘└──────────────────────┘┴ └┘└─────┘└─┘ └┘└────┘┴ └───┘
typ ─────────┘ └──────┘└───┘┴ ┴ └┘└──────────────────────┘┴ └┘└─────┘└─┘ └─┘└┘└────┘┴┴└───┘
doc ─────────┘ └──────┘ ┴ ┴ └┘ ┴ └┘ └─┘ └┘ ┴ └───┘
txt ─────────┘ └──────┘ ┴ ┴ └┘ ┴ └┘ └─┘ └┘ ┴ └───┘
par ─────────┘ └──────┘ ┴ ┴ └┘ ┴ └┘ └─┘ └┘ ┴ └───┘
pid ─────────┘ └──────┘ ┴ ┴ └┘ ┴ └┘ └─┘ └┘ ┴ └───┘
st ──────────────────────────────────────────────────────────────────────────────────────────┘└─
785 subrelation.wf this (measure_wf _)
id └────────────┘ └────────┘
src └────────────┘┴ ┴ └────────┘└───
typ └────────────┘┴ ┴ └────────┘└───
doc ┴ ┴ └───
txt ┴ ┴ └───
par ┴ ┴ └───
pid ┴ ┴ └─┘└
st ───────────────────────────────────
786
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
787 lemma preorder.well_founded [fintype α] [preorder α] : well_founded ((<) : α → α → Prop) :=
id └─────┘ ┴ └──────┘ ┴ └──────────┘ ┴ ┴ ┴
src └─────┘ └──────┘ └──────────┘ ┴
typ └─────┘ ┴ └──────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └─────┘
788 well_founded_of_trans_of_irrefl _
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
789
790 @[instance, priority 10] lemma linear_order.is_well_order [fintype α] [linear_order α] :
id └─────┘ ┴ └──────────┘ ┴
src └─────┘ └──────────┘
typ └─────┘ ┴ └──────────┘ ┴
doc └─────┘
791 is_well_order α (<) :=
id └───────────┘ ┴ ┴
src └───────────┘ ┴
typ └───────────┘ ┴ ┴
doc └───────────┘
792 { wf := preorder.well_founded }
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
793
794 end fintype
795
796 class infinite (α : Type*) : Prop :=
id └───┘
typ └───┘
797 (not_fintype : fintype α → false)
id └─────┘ ┴ ┴ └───┘
src └─────┘ └───┘
typ └─────┘ ┴ ┴ └───┘
doc └─────┘
798
799 @[simp] lemma not_nonempty_fintype {α : Type*} : ¬nonempty (fintype α) ↔ infinite α :=
id ┴└──────┘ └─────┘ ┴ ┴ └──────┘ ┴
src ┴└──────┘ └─────┘ ┴ └──────┘
typ ┴└──────┘ └─────┘ ┴ ┴ └──────┘ ┴
doc └──┘ └─────┘
800 ⟨λf, ⟨λ x, f ⟨x⟩⟩, λ⟨f⟩ ⟨x⟩, f x⟩
id ┴ ┴ ┴ ┴ ┴┴ ┴┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴┴
801
802 namespace infinite
803
804 lemma exists_not_mem_finset [infinite α] (s : finset α) : ∃ x, x ∉ s :=
id └──────┘ ┴ └────┘ ┴ ┴ ┴┴ ┴ ┴ ┴
src └──────┘ └────┘ ┴ ┴ ┴
typ └──────┘ ┴ └────┘ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └────┘
805 classical.not_forall.1 $ λ h, not_fintype ⟨s, h⟩
id └──────────────────┘┴ ┴ └─────────┘ ┴ ┴
src └──────────────────┘┴ └─────────┘
typ └──────────────────┘┴ ┴ └─────────┘ ┴ ┴
806
807 @[priority 100] -- see Note [lower instance priority]
808 instance nonempty (α : Type*) [infinite α] : nonempty α :=
id └──────┘ ┴ └──────┘ ┴
src └──────┘ └──────┘
typ └──────┘ ┴ └──────┘ ┴
809 nonempty_of_exists (exists_not_mem_finset (∅ : finset α))
id └────────────────┘ └───────────────────┘ ┴ └────┘ ┴
src └────────────────┘ └───────────────────┘ ┴ └────┘
typ └────────────────┘ └───────────────────┘ ┴ └────┘ ┴
doc └────┘
810
811 lemma of_injective [infinite β] (f : β → α) (hf : injective f) : infinite α :=
id └──────┘ ┴ ┴ ┴ └───────┘ ┴ └──────┘ ┴
src └──────┘ └───────┘ └──────┘
typ └──────┘ ┴ ┴ ┴ └───────┘ ┴ └──────┘ ┴
812 ⟨λ I, by exactI not_fintype (fintype.of_injective f hf)⟩
id ┴ └─────────┘ └──────────────────┘ ┴ └┘
src └─────┘└─────────┘┴ └──────────────────┘┴ ┴ ┴
typ ┴ └─────┘└─────────┘┴ └──────────────────┘┴┴┴└┘┴
doc └─────┘ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st └─────────────────────────────────────────────┘
813
814 lemma of_surjective [infinite β] (f : α → β) (hf : surjective f) : infinite α :=
id └──────┘ ┴ ┴ ┴ └────────┘ ┴ └──────┘ ┴
src └──────┘ └────────┘ └──────┘
typ └──────┘ ┴ ┴ ┴ └────────┘ ┴ └──────┘ ┴
815 ⟨λ I, by classical; exactI not_fintype (fintype.of_surjective f hf)⟩
id ┴ └─────────┘ └───────────────────┘ ┴ └┘
src └───────┘ └─────┘└─────────┘┴ └───────────────────┘┴ ┴ ┴
typ ┴ └───────┘ └─────┘└─────────┘┴ └───────────────────┘┴┴┴└┘┴
doc └───────┘ └─────┘ ┴ └───────────────────┘┴ ┴ ┴
txt └───────┘ └─────┘ ┴ ┴ ┴ ┴
par └───────┘ └─────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st └─────────────────────────────────────────────────────────┘
816
817 private noncomputable def nat_embedding_aux (α : Type*) [infinite α] : ℕ → α
id └──────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴
818 | n := by letI := classical.dec_eq α; exact classical.some (exists_not_mem_finset
id └──────────────┘ ┴ └────────────┘ └───────────────────┘
src └──────┘└──────────────┘┴ └────┘└────────────┘┴ └───────────────────┘└
typ └──────┘└──────────────┘┴┴ └────┘└────────────┘┴ └───────────────────┘└
doc └──────┘ ┴ └────┘ ┴ └
txt └──────┘ ┴ └────┘ ┴ └
par └──────┘ ┴ └────┘ ┴ └
pid ┴└─┘ ┴ ┴ ┴ └
st └────────────────────────────────────────────────────────────────────────
819 ((multiset.range n).pmap (λ m (hm : m < n), nat_embedding_aux m)
id └────────────┘ ┴ ┴ └───────────────┘
src ─┘ └────────────┘┴ └─────┘ └───────┘ ┴┴┴ └─┘ ┴ └─
typ ─┘ └────────────┘┴ └─────┘ └───────┘ ┴┴┴┴└─┘└───────────────┘┴ └─
doc ─┘ └────────────┘┴ └─────┘ └───────┘ ┴ ┴ └─┘ ┴ └─
txt ─┘ ┴ └─────┘ └───────┘ ┴ ┴ └─┘ ┴ └─
par ─┘ ┴ └─────┘ └───────┘ ┴ ┴ └─┘ ┴ └─
pid ─┘ ┴ └─────┘ └───────┘ ┴ ┴ └─┘ ┴ └─
st ───────────────────────────────────────────────────────────────────
820 (λ _, multiset.mem_range.1)).to_finset)
id └────────────────┘
src ───┘ └──┘└────────────────┘└───────────────
typ ───┘ └──┘└────────────────┘└───────────────
doc ───┘ └──┘ └───────────────
txt ───┘ └──┘ └───────────────
par ───┘ └──┘ └───────────────
pid ───┘ └──┘ └─────────────┘└
st ────────────────────────────────────────────
821
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
822 private lemma nat_embedding_aux_injective (α : Type*) [infinite α] :
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
823 function.injective (nat_embedding_aux α) :=
id └────────────────┘ └───────────────┘ ┴
src └────────────────┘ └───────────────┘
typ └────────────────┘ └───────────────┘ ┴
824 begin
st └─────
825 assume m n h,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └──────────┘
st ─────────────┘└─
826 letI := classical.dec_eq α,
id └──────────────┘ ┴
src └──────┘└──────────────┘┴
typ └──────┘└──────────────┘┴┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid ┴└─┘ ┴
st ───────────────────────────┘└─
827 wlog hmlen : m ≤ n using m n,
id ┴ ┴ ┴
src └───────────┘ ┴┴┴ └────────┘
typ └───────────┘┴┴┴┴┴└────────┘
doc └───────────┘ ┴ ┴ └────────┘
txt └───────────┘ ┴ ┴ └────────┘
par └───────────┘ ┴ ┴ └────────┘
pid └────┘└─┘ ┴ ┴ ┴└───────┘
st ─────────────────────────────┘└─
828 by_contradiction hmn,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └──┘
st ─────────────────────┘└─
829 have hmn : m < n, from lt_of_le_of_ne hmlen hmn,
id ┴ ┴ ┴ └────────────┘ └───┘ └─┘
src └─────────┘ ┴┴┴ └───┘└────────────┘┴ ┴
typ └─────────┘┴┴┴┴┴ └───┘└────────────┘┴└───┘┴└─┘
doc └─────────┘ ┴ ┴ └───┘ ┴ ┴
txt └─────────┘ ┴ ┴ └───┘ ┴ ┴
par └─────────┘ ┴ ┴ └───┘ ┴ ┴
pid └──────┘└─┘ ┴ ┴ └───┘ ┴ ┴
st ─────────────────┘└─────────────────────────────┘└─
830 refine (classical.some_spec (exists_not_mem_finset
id └─────────────────┘ └───────────────────┘
src └─────┘ └─────────────────┘┴ └───────────────────┘└
typ └─────┘ └─────────────────┘┴ └───────────────────┘└
doc └─────┘ ┴ └
txt └─────┘ ┴ └
par └─────┘ ┴ └
pid ┴ ┴ └
st ─────────────────────────────────────────────────────
831 ((multiset.range n).pmap (λ m (hm : m < n), nat_embedding_aux α m)
id └────────────┘ ┴ ┴ └───────────────┘ ┴
src ───┘ └────────────┘┴ └─────┘ └───────┘ ┴ ┴ └─┘└───────────────┘┴ ┴ └─
typ ───┘ └────────────┘┴ └─────┘ └───────┘ ┴┴┴┴└─┘└───────────────┘┴┴┴ └─
doc ───┘ └────────────┘┴ └─────┘ └───────┘ ┴ ┴ └─┘ ┴ ┴ └─
txt ───┘ ┴ └─────┘ └───────┘ ┴ ┴ └─┘ ┴ ┴ └─
par ───┘ ┴ └─────┘ └───────┘ ┴ ┴ └─┘ ┴ ┴ └─
pid ───┘ ┴ └─────┘ └───────┘ ┴ ┴ └─┘ ┴ ┴ └─
st ───────────────────────────────────────────────────────────────────────
832 (λ _, multiset.mem_range.1)).to_finset)) _,
id └────────────────┘
src ─────┘ └──┘└────────────────┘└────────────────┘
typ ─────┘ └──┘└────────────────┘└────────────────┘
doc ─────┘ └──┘ └────────────────┘
txt ─────┘ └──┘ └────────────────┘
par ─────┘ └──┘ └────────────────┘
pid ─────┘ └──┘ └────────────────┘
st ───────────────────────────────────────────────┘└─
833 refine multiset.mem_to_finset.2 (multiset.mem_pmap.2
id └────────────────────┘ └───────────────┘
src └─────┘└────────────────────┘└─┘ └───────────────┘└──
typ └─────┘└────────────────────┘└─┘ └───────────────┘└──
doc └─────┘ └─┘ └──
txt └─────┘ └─┘ └──
par └─────┘ └─┘ └──
pid ┴ └─┘ └──
st ───────────────────────────────────────────────────────
834 ⟨m, multiset.mem_range.2 hmn, _⟩),
id ┴ └────────────────┘ └─┘
src ───┘ └┘└────────────────┘└─┘ └───┘
typ ───┘ ┴└┘└────────────────┘└─┘└─┘└───┘
doc ───┘ └┘ └─┘ └───┘
txt ───┘ └┘ └─┘ └───┘
par ───┘ └┘ └─┘ └───┘
pid ───┘ └┘ └─┘ └───┘
st ────────────────────────────────────┘└─
835 rw [h, nat_embedding_aux]
id ┴ └───────────────┘
src └──┘ └┘└───────────────┘└┘
typ └──┘┴└┘└───────────────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st ──────┘└─────────────────┘┴┴
836 end
st └─┘
837
838 noncomputable def nat_embedding (α : Type*) [infinite α] : ℕ ↪ α :=
id └──────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴
839 ⟨_, nat_embedding_aux_injective α⟩
id └─────────────────────────┘ ┴
src └─────────────────────────┘
typ └─────────────────────────┘ ┴
840
841 end infinite
842
843 lemma not_injective_infinite_fintype [infinite α] [fintype β] (f : α → β) :
id └──────┘ ┴ └─────┘ ┴ ┴ ┴
src └──────┘ └─────┘
typ └──────┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘
844 ¬ injective f :=
id ┴ └───────┘ ┴
src ┴ └───────┘
typ ┴ └───────┘ ┴
845 assume (hf : injective f),
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
846 have H : fintype α := fintype.of_injective f hf,
id └─────┘ ┴ └──────────────────┘ ┴ └┘
src └─────┘ └──────────────────┘
typ └─────┘ ┴ └──────────────────┘ ┴ └┘
doc └─────┘
847 infinite.not_fintype H
id └──────────────────┘ ┴
src └──────────────────┘
typ └──────────────────┘ ┴
848
849 lemma not_surjective_fintype_infinite [fintype α] [infinite β] (f : α → β) :
id └─────┘ ┴ └──────┘ ┴ ┴ ┴
src └─────┘ └──────┘
typ └─────┘ ┴ └──────┘ ┴ ┴ ┴
doc └─────┘
850 ¬ surjective f :=
id ┴ └────────┘ ┴
src ┴ └────────┘
typ ┴ └────────┘ ┴
851 assume (hf : surjective f),
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
852 have H : infinite α := infinite.of_surjective f hf,
id └──────┘ ┴ └────────────────────┘ ┴ └┘
src └──────┘ └────────────────────┘
typ └──────┘ ┴ └────────────────────┘ ┴ └┘
853 @infinite.not_fintype _ H infer_instance
id └──────────────────┘ ┴ └────────────┘
src └──────────────────┘ └────────────┘
typ └──────────────────┘ ┴ └────────────┘
doc └────────────┘
854
855 instance nat.infinite : infinite ℕ :=
id └──────┘ ┴
src └──────┘ ┴
typ └──────┘ ┴
856 ⟨λ ⟨s, hs⟩, finset.not_mem_range_self $ s.subset_range_sup_succ (hs _)⟩
id ┴┴ └┘ └───────────────────────┘ └────────────────────┘
src └───────────────────────┘ └────────────────────┘
typ ┴┴ └┘ └───────────────────────┘ └────────────────────┘
857
858 instance int.infinite : infinite ℤ :=
id └──────┘ ┴
src └──────┘ ┴
typ └──────┘ ┴
859 infinite.of_injective int.of_nat (λ _ _, int.of_nat_inj)
id └───────────────────┘ └────────┘ ┴ ┴ └────────────┘
src └───────────────────┘ └────────┘ └────────────┘
typ └───────────────────┘ └────────┘ ┴ ┴ └────────────┘